3 let EGCD_INVARIANT = thm `;
4 !m n d. d divides egcd(m,n) <=> d divides m /\ d divides n
9 ==> (!d. d divides egcd (m'',n') <=>
10 d divides m'' /\ d divides n'))
11 ==> (!d. d divides egcd (m,n) <=> d divides m /\ d divides n) [1]
15 ==> (!d. d divides egcd (m'',n') <=>
16 d divides m'' /\ d divides n') [2];
23 else if m <= n then egcd (m,n - m) else egcd (m - n,n)) <=>
24 d divides m /\ d divides n [3]
27 m = 0 ==> (d divides n <=> d divides m /\ d divides n) [4]
34 if m <= n then egcd (m,n - m) else egcd (m - n,n)) <=>
35 d divides m /\ d divides n) [5]
38 n = 0 ==> (d divides m <=> d divides m /\ d divides n) [7]
42 (if m <= n then egcd (m,n - m) else egcd (m - n,n)) <=>
43 d divides m /\ d divides n) [8]
47 ==> (d divides egcd (m,n - m) <=>
48 d divides m /\ d divides n) [10]
51 m + (n - m) < m + n by ARITH_TAC,6;
54 ==> (d divides egcd (m - n,n) <=>
55 d divides m /\ d divides n) [11]
58 (m - n) + n < m + n by ARITH_TAC,9;
59 d divides egcd (m - n,n) <=> d divides m - n /\ d divides n
61 ... <=> d divides (m - n) + n /\ d divides n by DIVIDES_ADD;
66 qed by COND_CASES_TAC from 10,11;
67 qed by COND_CASES_TAC from 7,8;
68 qed by COND_CASES_TAC from 4,5;
69 qed by ONCE_REWRITE_TAC[egcd] from 3;
70 qed by WF_INDUCT_TAC (parse_term "m + n") from 1;