Prove that \(I {\ \land \ }B \to {wp\left(V_1 := V; S, V < V_1\right)}\).
\[\begin{split} & I {\ \land \ }B \to {wp\left(V_1 := V; S, V < V_1\right)}\\ {\ ({\mathbf{§2}})} \iff & I {\ \land \ }B \to {wp\left(V_1 := n, {wp\left(res := res + m, {wp\left(n := n - 1, n < V_1\right)}\right)}\right)}\\ {\ ({\mathbf{§1}})} \iff & I {\ \land \ }B \to {wp\left(V_1 := n, {wp\left(res := res + m, n - 1 < V_1\right)}\right)}\\ {\ ({\mathbf{§1}})} \iff & I {\ \land \ }B \to {wp\left(V_1 := n, n - 1 < V_1\right)}\\ {\ ({\mathbf{§1}})} \iff & I {\ \land \ }B \to n - 1 < n\\ \iff & (res + nm = n_0m_0) {\ \land \ }(n \geq 0) {\ \land \ }(0 < n) \to n - 1 < n\\ \iff & {{\mathbf{\top}}}\\ \end{split}\]
It is trivially true since \(\forall n \in \mathbb{Z} : n - 1 < n = {{\mathbf{\top}}}\). It is easy to see that the variant decreases.