Upon loop termination

Prove that \(I {\ \land \ }\neg B \to R\).

\[\begin{split} & I {\ \land \ }\neg B \to R\\ \iff & (i \leq n + 1) {\ \land \ }(res = (i - 1)!) {\ \land \ }(i > n) \to res = n!\\ \iff & (i = n + 1) {\ \land \ }(res = (i - 1)!) \to res = n!\\ \iff & res = n! \to res = n!\\ \end{split}\]