Okay so I started reading The Art of Computer Programming and have started doing the exercises but am having a bit of difficulty with formal proofs. I'm not that great with maths but would like to get better so this is my attempt. One of the (supposed) easy exercises states: Prove that m is always greater than n at the beginning of step E1. except possibly the first time the step occurs. The algorithm is as follows: E1 [Find the remainder] Divide m by n and let r be the remainder. (We will have 0 <= r < n). E2 [Is it 0?] If r = 0, the algorithm terminates; n is the answer. E3 [Reduce] Set m <- n, n <- r, and go back to step E1. Okay so we do: E1 m = 3 and n = 5. 3 / 5 = 0 r = 3. E2 r = 3, continue E3 m = 5, n = 3 E1 5 / 3 = 1 r = 2 E2 r = 2, continue E3 m = 3, n = 2 E1 3 / 2 = 1 r = 1 E2 r = 1, continue E3 m = 2, n = 1 E1 2 / 1 = 2 r = 0 E2 r = 0, terminate If n > m then at step E3 m => n meaning that after one iteration n is always <= m. How would I write this as a formal proof? Am I doing anything wrong?