Problem Episode on proving the program is correct

Question.
Prove that if quotRem(n,m) is called with arguments that satisfy the precondition, it terminates, and
when it does it satises the postcondition.
def quotRem(n,m) :
# Precondition: n,m are natural numbers
# m is not 0
r = n
q = 0
while (not (m > r)) :
r = r - m
q = q + 1
# Postcondition: n = qm + r and 0 <= r < m
return [q, r]

UNDERSTANDING THE PROBLEM
Given a program with a while loop. We need to prove that the program
acturally terninates and the precondition implies the postcondition.
For each while loop, r decreases by m, and q increment by 1. Since the
loop condition is on r, which is a decreasing natural number, thus the
while loop will terninate. We will show the correctness of the program by
proving using induction.

DEVISING A PLAN
1) Prove that for each loop, the loop invariant is correct.
2) Prove the while loop acturally terminates.
This proof need 2 steps: 1st is to prove that the loop invariant is in a strictly
decreasing sequence. Then by PWO , we show that the loop terminates.
3) Prove that the precondition implies the postcondition. This step is simple,
since we have shown most of the needed condition in 1) and 2).

CARRYING OUT THE PLAN
1)
Let P(i) be if there is i iterations, if the precondition is true,
then n = q_i * m + r_i and 0 <= r_i < m is a natural number.
Claim 1a: for all natural number i, P(i).
Proof.
Base case: If i = 0, then r_0 = n by line 1 and q_0 = 0 by line 2.
So n = 0 + n = q_0 + r_0. Since the loop does not execute,(0 iteration)
it's obvious that the condition (not m > r) fails,
so m is greater than r_0. Since r_0 = n is a natural number by precondition,
r_0 >= 0. So we have 0 <= r_0 < m. So P(0) is true.

Induction step: Assume that P(i) is true for any natural number i.
We need to show that P(i+1) is true.
If there is no (i+1)th iteration of the loop, P(i) is vacuously true.
Otherwise, assume there is (i+1)th iteration and precondition holds.
r_(i+1) = r_i - m by line 4, q_(i+1) = q_i + 1.
n = q_i * m + r_i (by IH) = q_i * m + r_i + m - m
= m *(q_i + 1) + (r_i - m)
= m * (q_(i+1)) + r_(i+1)
Hence P(i+1) is true.

We have shown that P(i) implies P(i+1) for any natural number i,
So we have P(i) for any natural number i.

2)
Claim 1b: Let E_i = r_i - m be a natural number. If m <= n,
m is a positive natural number, then E_i is a strictly decreasing sequence.
Proof: Base case: if m = n, then E_0 = n - m = 0. E_1 = r_1 - m = 0 - m < 0.
E_1 is not a natural number, so the set E_i only contains 0, we can
say that this is a strictly decreasing sequence.

Induction step: if m < n, and there is (i+1) iterations,
then r_(i+1) = r_i - m. We have
E_(i+1) = r_(i+1) - m = (r_i - m) - m = r_i - 2m.
By precondition, we know that m is not equal to 0 and m is a natural number.
So m > 0, and r_i - 2m < r_i - m, which implies E_(i+1) < E_i. Thus E is a
strictly decreasing sequence.

Hence E_i is a strictly decreasing sequence.

Claim 1c: quotRem(n,m) terminates.
Proof: n,m are natural numbers. If m > n, then we are done since the loop will
not execute and so will terminate. Otherwise, m <= n, the the loop will execute.
We have shown that natural number E_i = r_i - m is a strictly decreasing sequance
and non-empty since it contains at least E_0 = r_i - m = n - m >= 0.
Then by Principle of Well Ordering, there is a least value, say E_k, which must
also be last (strictly decreasing), which means there is no (k + 1)th iteration
of the loop. Thus the loop terminates.

3)
Claim 1d: If precondition is true, then the postcondition is true.
Proof. We have shown that the precondition implies that the loop terminates and
for each loop n = q_i * m + r_i and 0 <= r_i < m.
Thus for the last loop n = q_k * m + r_k and 0 <= r_i < m, and the loop
terminates. Write this form without indicating the subscript, we have
n = q*m + r and 0 <= r < m, satisfying the postcondition.
Therefore, the precondition implies the postcondition.

Looking Back
This episode can be used to prove most of the question on correctness of the program.