Upon loop termination

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

\[\begin{split} & I {\ \land \ }\neg B \to R\\ \iff & (res + nm = n_0m_0) {\ \land \ }(n \geq 0) {\ \land \ }(0 \geq n) \to (res = n_0m_0)\\ \iff & (res + nm = n_0m_0) {\ \land \ }(n = 0) \to (res = n_0m_0)\\ \iff & (res + 0 * m = n_0m_0) \to (res = n_0m_0)\\ \iff & (res = n_0m_0) \to (res = n_0m_0)\\ \iff & {{\mathbf{\top}}}\end{split}\]