Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 24 Nov 1993 20:48:14 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA04510;
          Wed, 24 Nov 1993 13:32:24 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA04506;
          Wed, 24 Nov 1993 13:30:55 -0700
Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA07275; Wed, 24 Nov 93 12:27:50 -0800
Received: from guillemot.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Wed, 24 Nov 1993 20:27:28 +0000
To: Info-hol <info-hol@cs.uidaho.edu>
Subject: Easy case of Fermat's Last Theorem
Date: Wed, 24 Nov 93 20:27:18 +0000
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:268690:931124202746"@cl.cam.ac.uk>


There's been a lot of publicity recently about Wiles' proof of Fermat's Last
Theorem and whether it is correct. It would be nice to computer-check it, but
that's a pretty major undertaking. However I thought it would be fun to prove
the one really elementary case (the one Fermat actually proved) which is n=4
(and hence all multiples of 4 of course) in HOL.

The proof was not so hard, but required quite a lot of groundwork concerning
divisibility, greatest common divisor, coprimality and primality. A few of
these theorems are not actually needed in the proof but are included for the
sake of completeness. Note that they concern the natural numbers, not the
integers or a more general ring. Then we prove a parametrization theorem for
Pythagorean triples (this can also be obtained geometrically) and then FLT
follows with a bit of tedious hacking.

A more interesting challenge would be to prove the n=3 case. At LPAR-93,
Grigori Mints was adamant that even this is beyond the capacity of current
proofcheckers. I am quite sure he is wrong, and said so, but I'm not prepared
to invest the effort involved in proving it. Anybody have a few weeks spare and
want to try?

Anyway, I hope this proof is of some interest in itself and provides some
useful theorems for other people working in this area. I'm afraid the proofs
are rather unpolished and the theorems rather illogically named.

John.

%============================================================================%
% Easy (relatively) n=4 case of FLT                                          %
%============================================================================%

timer true;;

load_library `reduce`;;

can unlink `FERMAT.th`;;

new_theory `FERMAT`;;

%----------------------------------------------------------------------------%
% Useful tactics.                                                            %
%----------------------------------------------------------------------------%

let TAUT_CONV =
  let val w t = type_of t = ":bool" & can (find_term is_var) t & free_in t w in
  C (curry prove)
  (REPEAT GEN_TAC THEN (REPEAT o CHANGED_TAC o W)
   (C $THEN (REWRITE_TAC[]) o BOOL_CASES_TAC o hd o sort (uncurry free_in) o
    W(find_terms o val) o snd));;

let LAND_CONV = RATOR_CONV o RAND_CONV;;

let ANTE_RES_THEN ttac th = FIRST_ASSUM(\t. ttac (MATCH_MP t th));;

let IMP_RES_THEN ttac th = FIRST_ASSUM(\t. ttac (MATCH_MP th t));;

%----------------------------------------------------------------------------%
% We want to use complete induction, so package it up.                       %
%----------------------------------------------------------------------------%

let COMPLETE_INDUCTION = prove_thm(`COMPLETE_INDUCTION`,
  "!P. (!n. (!m. m < n ==> P m) ==> P n) ==> !n. P n",
  let wopeta = CONV_RULE(ONCE_DEPTH_CONV ETA_CONV) WOP in
  GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN
  CONV_TAC(ONCE_DEPTH_CONV NOT_FORALL_CONV) THEN
  DISCH_THEN(MP_TAC o MATCH_MP wopeta) THEN BETA_TAC THEN
  REWRITE_TAC[NOT_IMP] THEN DISCH_THEN(X_CHOOSE_TAC "n:num") THEN
  EXISTS_TAC "n:num" THEN ASM_REWRITE_TAC[]);;

let COMPLETE_INDUCT_TAC =
  W(MATCH_MP_TAC o CONV_RULE (ONCE_DEPTH_CONV BETA_CONV) o
    C SPEC COMPLETE_INDUCTION o rand o snd);;

%----------------------------------------------------------------------------%
% General arithmetic lemmas.                                                 %
%----------------------------------------------------------------------------%

let MULT_EQ_1 = prove_thm(`MULT_EQ_1`,
  "!x y. (x * y = 1) = (x = 1) /\ (y = 1)",
  REPEAT GEN_TAC THEN
  STRUCT_CASES_TAC(SPEC "x:num" num_CASES) THEN
  STRUCT_CASES_TAC(SPEC "y:num" num_CASES) THEN
  REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; num_CONV "1";
    INV_SUC_EQ; SUC_NOT; ADD_EQ_0] THEN
  EQ_TAC THEN DISCH_TAC THEN
  ASM_REWRITE_TAC[MULT_CLAUSES]);;

let MULT_FIX = prove_thm(`MULT_FIX`,
  "!x y. (x * y = x) = (x = 0) \/ (y = 1)",
  REPEAT GEN_TAC THEN
  STRUCT_CASES_TAC(SPEC "x:num" num_CASES) THEN
  REWRITE_TAC[MULT_CLAUSES; NOT_SUC] THEN
  REWRITE_TAC[SYM(el 5 (CONJUNCTS (SPEC_ALL MULT_CLAUSES)))] THEN
  GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) []
   [SYM(el 4 (CONJUNCTS(SPEC_ALL MULT_CLAUSES)))] THEN
  MATCH_ACCEPT_TAC MULT_MONO_EQ);;

let LESS_EQ_MULT = prove_thm(`LESS_EQ_MULT`,
  "!m n p q. m <= n /\ p <= q ==> (m * p) <= (n * q)",
  REPEAT GEN_TAC THEN
  DISCH_THEN(STRIP_ASSUME_TAC o REWRITE_RULE[LESS_EQ_EXISTS]) THEN
  ASM_REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB;
    GSYM ADD_ASSOC; LESS_EQ_ADD]);;

let LESS_MULT = prove_thm(`LESS_MULT`,
  "!m n p q. m < n /\ p < q ==> (m * p) < (n * q)",
  REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN
   ((CHOOSE_THEN SUBST_ALL_TAC) o MATCH_MP LESS_ADD_1)) THEN
  REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
  REWRITE_TAC[GSYM ADD1; MULT_CLAUSES; ADD_CLAUSES; GSYM ADD_ASSOC] THEN
  ONCE_REWRITE_TAC[GSYM (el 4 (CONJUNCTS ADD_CLAUSES))] THEN
  MATCH_ACCEPT_TAC LESS_ADD_SUC);;

let MULT_LCANCEL = prove_thm(`MULT_LCANCEL`,
  "!a b c. ~(a = 0) /\ (a * b = a * c) ==> (b = c)",
  REPEAT GEN_TAC THEN STRUCT_CASES_TAC(SPEC "a:num" num_CASES) THEN
  REWRITE_TAC[NOT_SUC; MULT_MONO_EQ]);;

let LESS_EQ_ANTISYM_EQ = prove_thm(`LESS_EQ_ANTISYM_EQ`,
  "!x y. x <= y /\ y <= x = (x = y)",
  REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[LESS_EQUAL_ANTISYM] THEN
  DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[LESS_EQ_REFL]);;

%----------------------------------------------------------------------------%
% Properties of the exponential function.                                    %
%----------------------------------------------------------------------------%

let EXP_0 = prove_thm(`EXP_0`,
  "!n. 0 EXP (SUC n) = 0",
  REWRITE_TAC[EXP; MULT_CLAUSES]);;

let EXP_1 = prove_thm(`EXP_1`,
  "!n. 1 EXP n = 1",
  INDUCT_TAC THEN ASM_REWRITE_TAC[MULT_CLAUSES; EXP]);;

let EXP_2 = prove_thm(`EXP_2`,
  "!x. x EXP 2 = x * x",
  REWRITE_TAC[num_CONV "2"; num_CONV "1"; EXP; MULT_CLAUSES; ADD_CLAUSES]);;

let MULT_EXP = prove_thm(`MULT_EXP`,
  "!n x y. (x * y) EXP n = (x EXP n) * (y EXP n)",
  INDUCT_TAC THEN ASM_REWRITE_TAC[EXP; MULT_CLAUSES] THEN
  REPEAT GEN_TAC THEN CONV_TAC(AC_CONV(MULT_ASSOC,MULT_SYM)));;

let EXP_EQ_0 = prove_thm(`EXP_EQ_0`,
  "!x n. (x EXP n = 0) = (x = 0) /\ ~(n = 0)",
  REPEAT GEN_TAC THEN EQ_TAC THENL
   [SPEC_TAC("n:num","n:num") THEN INDUCT_TAC THEN
    REWRITE_TAC[EXP] THEN REDUCE_TAC THEN
    REWRITE_TAC[MULT_EQ_0] THEN STRIP_TAC THEN
    ASM_REWRITE_TAC[NOT_SUC] THEN
    FIRST_ASSUM(IMP_RES_THEN ASSUME_TAC) THEN
    ASM_REWRITE_TAC[];
    STRUCT_CASES_TAC(SPEC "n:num" num_CASES) THEN
    REWRITE_TAC[EXP; NOT_SUC; MULT_EQ_0] THEN
    STRIP_TAC THEN ASM_REWRITE_TAC[]]);;

let EXP_EQ_1 = prove_thm(`EXP_EQ_1`,
  "!x n. (x EXP n = 1) = (x = 1) \/ (n = 0)",
  REPEAT GEN_TAC THEN STRUCT_CASES_TAC(SPEC "n:num" num_CASES) THEN
  ASM_REWRITE_TAC[EXP; NOT_SUC; MULT_EQ_1] THEN
  EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[EXP_1]);;

let EXP_MONO_LEMMA = prove_thm(`EXP_MONO_LEMMA`,
  "!n x y. x < y ==> (x EXP (SUC n)) < (y EXP (SUC n))",
  INDUCT_TAC THEN REWRITE_TAC[EXP; MULT_CLAUSES] THEN
  REWRITE_TAC[GSYM EXP] THEN ONCE_REWRITE_TAC[EXP] THEN
  REPEAT STRIP_TAC THEN MATCH_MP_TAC LESS_MULT THEN
  ASM_REWRITE_TAC[] THEN FIRST_ASSUM MATCH_MP_TAC THEN
  ASM_REWRITE_TAC[]);;

let EXP_MONO_LT = prove_thm(`EXP_MONO_LT`,
  "!n x y. (x EXP (SUC n)) < (y EXP (SUC n)) = (x < y)",
  REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[EXP_MONO_LEMMA] THEN
  CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[NOT_LESS; LESS_OR_EQ] THEN
  DISCH_THEN DISJ_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
  DISJ1_TAC THEN MATCH_MP_TAC EXP_MONO_LEMMA THEN ASM_REWRITE_TAC[]);;

let EXP_MONO_LE = prove_thm(`EXP_MONO_LE`,
  "!x y n. (x EXP (SUC n)) <= (y EXP (SUC n)) = x <= y",
  REWRITE_TAC[GSYM NOT_LESS; EXP_MONO_LT]);;

let EXP_MONO_EQ = prove_thm(`EXP_MONO_EQ`,
  "!x y n. (x EXP (SUC n) = y EXP (SUC n)) = (x = y)",
  REPEAT GEN_TAC THEN REWRITE_TAC[GSYM LESS_EQ_ANTISYM_EQ] THEN
  REWRITE_TAC[EXP_MONO_LE]);;

let EXP_EXP = prove_thm(`EXP_EXP`,
  "!x m n. (x EXP m) EXP n = x EXP (m * n)",
  GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
  ASM_REWRITE_TAC[EXP; MULT_CLAUSES; EXP_ADD]);;

%----------------------------------------------------------------------------%
% More ad-hoc arithmetic lemmas unlikely to be useful elsewhere.             %
%----------------------------------------------------------------------------%

let DIFF_LEMMA = prove_thm(`DIFF_LEMMA`,
  "!a b. a < b ==> (a = 0) \/ (a + (b - a)) < (a + b)",
  REPEAT GEN_TAC THEN
  DISJ_CASES_TAC(SPEC "a:num" LESS_0_CASES) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(CHOOSE_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1) THEN
  DISJ2_TAC THEN REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
  GEN_REWRITE_TAC LAND_CONV [] [GSYM (CONJUNCT1 ADD_CLAUSES)] THEN
  REWRITE_TAC[ADD_ASSOC] THEN
  REPEAT(MATCH_MP_TAC LESS_MONO_ADD) THEN POP_ASSUM ACCEPT_TAC);;

let NOT_EVEN_EQ_ODD = prove_thm(`NOT_EVEN_EQ_ODD`,
  "!m n. ~(2 * m = SUC(2 * n))",
  REWRITE_TAC[TIMES2; GSYM NOT_ODD_EQ_EVEN]);;

let CANCEL_TIMES2 = prove_thm(`CANCEL_TIMES2`,
  "!x y. (2 * x = 2 * y) = (x = y)",
  REWRITE_TAC[num_CONV "2"; MULT_MONO_EQ]);;

let EVEN_SQUARE = prove_thm(`EVEN_SQUARE`,
  "!n. EVEN(n) ==> ?x. n EXP 2 = 4 * x",
  GEN_TAC THEN REWRITE_TAC[EVEN_EXISTS] THEN
  DISCH_THEN(X_CHOOSE_THEN "m:num" SUBST1_TAC) THEN
  EXISTS_TAC "m * m" THEN REWRITE_TAC[EXP_2] THEN
  REWRITE_TAC[SYM(REDUCE_CONV "2 * 2")] THEN
  CONV_TAC(AC_CONV(MULT_ASSOC,MULT_SYM)));;

let ODD_SQUARE = prove_thm(`ODD_SQUARE`,
  "!n. ODD(n) ==> ?x. n EXP 2 = (4 * x) + 1",
  GEN_TAC THEN REWRITE_TAC[ODD_EXISTS] THEN
  DISCH_THEN(X_CHOOSE_THEN "m:num" SUBST1_TAC) THEN
  ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES; ADD_CLAUSES] THEN
  REWRITE_TAC[GSYM ADD1; INV_SUC_EQ] THEN
  EXISTS_TAC "(m * m) + m" THEN
  REWRITE_TAC(map num_CONV ["4"; "3"; "2"; "1"]) THEN
  REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
  REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
  CONV_TAC(AC_CONV(ADD_ASSOC,ADD_SYM)));;

let DIFF_SQUARE = prove_thm(`DIFF_SQUARE`,
  "!x y. (x EXP 2) - (y EXP 2) = (x + y) * (x - y)",
  REPEAT GEN_TAC THEN
  DISJ_CASES_TAC(SPECL ["x:num"; "y:num"] LESS_EQ_CASES) THENL
   [SUBGOAL_THEN "(x * x) <= (y * y)" MP_TAC THENL
     [MATCH_MP_TAC LESS_EQ_MULT THEN ASM_REWRITE_TAC[];
      POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM SUB_EQ_0] THEN
      REPEAT DISCH_TAC THEN ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES]];
    POP_ASSUM(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LESS_EQ_EXISTS]) THEN
    REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
    REWRITE_TAC[EXP_2; LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
    REWRITE_TAC[GSYM ADD_ASSOC; ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
    AP_TERM_TAC THEN GEN_REWRITE_TAC LAND_CONV [] [ADD_SYM] THEN
    AP_TERM_TAC THEN MATCH_ACCEPT_TAC MULT_SYM]);;

let ADD_IMP_SUB = prove_thm(`ADD_IMP_SUB`,
  "!x y z. (x + y = z) ==> (x = z - y)",
  REPEAT GEN_TAC THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
  REWRITE_TAC[ADD_SUB]);;

let ADD_SUM_DIFF = prove_thm(`ADD_SUM_DIFF`,
  "!v w. v <= w ==> ((w + v) - (w - v) = 2 * v) /\
                    ((w + v) + (w - v) = 2 * w)",
  REPEAT GEN_TAC THEN REWRITE_TAC[LESS_EQ_EXISTS] THEN
  DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN
  REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN
  REWRITE_TAC[TIMES2; GSYM ADD_ASSOC] THEN
  ONCE_REWRITE_TAC[ADD_SYM] THEN
  REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB; GSYM ADD_ASSOC]);;

let EXP_4 = prove_thm(`EXP_4`,
  "!n. n EXP 4 = (n EXP 2) EXP 2",
  GEN_TAC THEN REWRITE_TAC[EXP_EXP] THEN
  REDUCE_TAC THEN REFL_TAC);;

%----------------------------------------------------------------------------%
% Elementary theory of divisibility                                          %
%----------------------------------------------------------------------------%

let divides = new_infix_definition(`divides`,
  "$divides a b = ?x. b = a * x");;

let DIVIDES_0 = prove_thm(`DIVIDES_0`,
  "!x. x divides 0",
  GEN_TAC THEN REWRITE_TAC[divides] THEN
  EXISTS_TAC "0" THEN REWRITE_TAC[MULT_CLAUSES]);;

let DIVIDES_ZERO = prove_thm(`DIVIDES_ZERO`,
  "!x. 0 divides x = (x = 0)",
  GEN_TAC THEN REWRITE_TAC[divides] THEN
  EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[MULT_CLAUSES]);;

let DIVIDES_1 = prove_thm(`DIVIDES_1`,
  "!x. 1 divides x",
  GEN_TAC THEN REWRITE_TAC[divides] THEN
  EXISTS_TAC "x:num" THEN REWRITE_TAC[MULT_CLAUSES]);;

let DIVIDES_ONE = prove_thm(`DIVIDES_ONE`,
  "!x. (x divides 1) = (x = 1)",
  GEN_TAC THEN REWRITE_TAC[divides] THEN
  CONV_TAC(LAND_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN
  REWRITE_TAC[MULT_EQ_1] THEN EQ_TAC THEN STRIP_TAC THEN
  ASM_REWRITE_TAC[] THEN EXISTS_TAC "1" THEN REFL_TAC);;

let DIVIDES_GE = prove_thm(`DIVIDES_GE`,
  "!a b. a divides b ==> (b = 0) \/ a <= b",
  REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
  DISCH_THEN(X_CHOOSE_THEN "x:num" SUBST1_TAC) THEN
  STRUCT_CASES_TAC(SPEC "x:num" num_CASES) THEN
  REWRITE_TAC[MULT_CLAUSES; LESS_EQ_ADD]);;

let DIVIDES_REFL = prove_thm(`DIVIDES_REFL`,
  "!x. x divides x",
  GEN_TAC THEN REWRITE_TAC[divides] THEN
  EXISTS_TAC "1" THEN REWRITE_TAC[MULT_CLAUSES]);;

let DIVIDES_TRANS = prove_thm(`DIVIDES_TRANS`,
  "!a b c. a divides b /\ b divides c ==> a divides c",
  REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
  DISCH_THEN (CONJUNCTS_THEN MP_TAC) THEN
  REPEAT(DISCH_THEN(CHOOSE_THEN SUBST1_TAC)) THEN
  REWRITE_TAC[GSYM MULT_ASSOC] THEN
  W(EXISTS_TAC o rand o lhs o snd o dest_exists o snd) THEN
  REFL_TAC);;

let DIVIDES_ANTISYM = prove_thm(`DIVIDES_ANTISYM`,
  "!x y. x divides y /\ y divides x = (x = y)",
  REPEAT GEN_TAC THEN EQ_TAC THENL
   [REWRITE_TAC[divides] THEN
    DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (CHOOSE_THEN SUBST1_TAC)) THEN
    DISCH_THEN(CHOOSE_THEN MP_TAC) THEN
    CONV_TAC(LAND_CONV SYM_CONV) THEN
    REWRITE_TAC[GSYM MULT_ASSOC; MULT_FIX; MULT_EQ_1] THEN
    STRIP_TAC THEN ASM_REWRITE_TAC[];
    DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[DIVIDES_REFL]]);;

let DIVIDES_ADD = prove_thm(`DIVIDES_ADD`,
  "!d a b. d divides a /\ d divides b ==> d divides (a + b)",
  REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
  DISCH_THEN(CONJUNCTS_THEN (CHOOSE_THEN SUBST1_TAC)) THEN
  REWRITE_TAC[GSYM LEFT_ADD_DISTRIB] THEN
  W(EXISTS_TAC o rand o lhs o snd o dest_exists o snd) THEN
  REFL_TAC);;

let DIVIDES_SUB = prove_thm(`DIVIDES_SUB`,
  "!d a b. d divides a /\ d divides b ==> d divides (a - b)",
  REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
  DISCH_THEN(CONJUNCTS_THEN (CHOOSE_THEN SUBST1_TAC)) THEN
  REWRITE_TAC[GSYM LEFT_SUB_DISTRIB] THEN
  W(EXISTS_TAC o rand o lhs o snd o dest_exists o snd) THEN
  REFL_TAC);;

let DIVIDES_LMUL = prove_thm(`DIVIDES_LMUL`,
  "!d a x. d divides a ==> d divides (x * a)",
  REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
  DISCH_THEN(X_CHOOSE_THEN "p:num" SUBST1_TAC) THEN
  EXISTS_TAC "x * p" THEN
  CONV_TAC(AC_CONV(MULT_ASSOC,MULT_SYM)));;

let DIVIDES_RMUL = prove_thm(`DIVIDES_RMUL`,
  "!d a x. d divides a ==> d divides (a * x)",
  ONCE_REWRITE_TAC[MULT_SYM] THEN MATCH_ACCEPT_TAC DIVIDES_LMUL);;

let DIVIDES_ADD_REVR = prove_thm(`DIVIDES_ADD_REVR`,
  "!d a b. d divides a /\ d divides (a + b) ==> d divides b",
  REPEAT GEN_TAC THEN DISCH_TAC THEN
  SUBST1_TAC(SYM(SPECL ["b:num"; "a:num"] ADD_SUB)) THEN
  ONCE_REWRITE_TAC[ADD_SYM] THEN
  MATCH_MP_TAC DIVIDES_SUB THEN ASM_REWRITE_TAC[]);;

let DIVIDES_ADD_REVL = prove_thm(`DIVIDES_ADD_REVL`,
  "!d a b. d divides b /\ d divides (a + b) ==> d divides a",
  ONCE_REWRITE_TAC[ADD_SYM] THEN MATCH_ACCEPT_TAC DIVIDES_ADD_REVR);;

let DIVIDES_DIV = prove_thm(`DIVIDES_DIV`,
  "!n x. 0 < n /\ (x MOD n = 0) ==> n divides x",
  REPEAT STRIP_TAC THEN
  FIRST_ASSUM(MP_TAC o SPEC "x:num" o MATCH_MP DIVISION) THEN
  ASM_REWRITE_TAC[ADD_CLAUSES] THEN DISCH_TAC THEN
  REWRITE_TAC[divides] THEN EXISTS_TAC "x DIV n" THEN
  ONCE_REWRITE_TAC[MULT_SYM] THEN FIRST_ASSUM MATCH_ACCEPT_TAC);;

let DIVIDES_MUL_L = prove_thm(`DIVIDES_MUL_L`,
  "!a b c. a divides b ==> (c * a) divides (c * b)",
  REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
  DISCH_THEN(X_CHOOSE_THEN "x:num" SUBST1_TAC) THEN
  EXISTS_TAC "x:num" THEN REWRITE_TAC[MULT_ASSOC]);;

let DIVIDES_MUL_R = prove_thm(`DIVIDES_MUL_R`,
  "!a b c. a divides b ==> (a * c) divides (b * c)",
  ONCE_REWRITE_TAC[MULT_SYM] THEN MATCH_ACCEPT_TAC DIVIDES_MUL_L);;

let DIVIDES_LMUL2 = prove_thm(`DIVIDES_LMUL2`,
  "!d a x. (x * d) divides a ==> d divides a",
  REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
  DISCH_THEN(X_CHOOSE_THEN "y:num" SUBST1_TAC) THEN
  EXISTS_TAC "x * y" THEN
  CONV_TAC(AC_CONV(MULT_ASSOC,MULT_SYM)));;

let DIVIDES_RMUL2 = prove_thm(`DIVIDES_RMUL2`,
  "!d a x. (d * x) divides a ==> d divides a",
  ONCE_REWRITE_TAC[MULT_SYM] THEN
  MATCH_ACCEPT_TAC DIVIDES_LMUL2);;

let DIVIDES_CMUL2 = prove_thm(`DIVIDES_CMUL2`,
  "!a b c. (c * a) divides (c * b) /\ ~(c = 0) ==> a divides b",
  REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
  DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC "x:num") ASSUME_TAC) THEN
  EXISTS_TAC "x:num" THEN MATCH_MP_TAC MULT_LCANCEL THEN
  EXISTS_TAC "c:num" THEN ASM_REWRITE_TAC[MULT_ASSOC]);;

let DIVIDES_LE = prove_thm(`DIVIDES_LE`,
  "!m n. m divides n ==> m <= n \/ (n = 0)",
  REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
  DISCH_THEN(X_CHOOSE_THEN "x:num" SUBST1_TAC) THEN
  REWRITE_TAC[MULT_EQ_0] THEN
  STRUCT_CASES_TAC(SPEC "x:num" num_CASES) THEN
  ASM_REWRITE_TAC[MULT_CLAUSES; LESS_EQ_ADD]);;

let DIVIDES_DIV_NOT = prove_thm(`DIVIDES_DIV_NOT`,
  "!n x q r. (x = (q * n) + r) /\ 0 < r /\ r < n ==> ~(n divides x)",
  REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
  MP_TAC(SPEC "n:num" DIVIDES_REFL) THEN
  DISCH_THEN(MP_TAC o SPEC "q:num" o MATCH_MP DIVIDES_LMUL) THEN
  PURE_REWRITE_TAC[TAUT_CONV "a ==> ~b = a /\ b ==> F"] THEN
  DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_ADD_REVR) THEN
  DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN
  ASM_REWRITE_TAC[DE_MORGAN_THM; NOT_LESS_EQUAL; GSYM LESS_EQ_0]);;

let DIVIDES_MUL2 = prove_thm(`DIVIDES_MUL2`,
  "!a b c d. a divides b /\ c divides d ==> (a * c) divides (b * d)",
  REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
  DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC "x:num")
   (X_CHOOSE_TAC "y:num")) THEN EXISTS_TAC "x * y" THEN
  ASM_REWRITE_TAC[] THEN
  CONV_TAC(AC_CONV(MULT_ASSOC,MULT_SYM)));;

let DIVIDES_EXP = prove_thm(`DIVIDES_EXP`,
  "!x y n. x divides y ==> (x EXP n) divides (y EXP n)",
  REPEAT GEN_TAC THEN REWRITE_TAC[divides] THEN
  DISCH_THEN(X_CHOOSE_THEN "d:num" SUBST1_TAC) THEN
  EXISTS_TAC "d EXP n" THEN MATCH_ACCEPT_TAC MULT_EXP);;

let DIVIDES_EXP2 = prove_thm(`DIVIDES_EXP2`,
  "!n x y. ~(n = 0) /\ (x EXP n) divides y ==> x divides y",
  INDUCT_TAC THEN REWRITE_TAC[NOT_SUC] THEN
  REPEAT GEN_TAC THEN REWRITE_TAC[EXP] THEN
  DISCH_TAC THEN FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) THEN
  DISCH_THEN(MP_TAC o SPECL ["x:num"; "y:num"]) THEN
  POP_ASSUM MP_TAC THEN STRUCT_CASES_TAC(SPEC "n:num" num_CASES) THENL
   [REWRITE_TAC[EXP; MULT_CLAUSES];
    DISCH_TAC THEN REWRITE_TAC[NOT_SUC] THEN
    DISCH_THEN MATCH_MP_TAC THEN
    MATCH_MP_TAC DIVIDES_LMUL2 THEN
    EXISTS_TAC "x:num" THEN ASM_REWRITE_TAC[]]);;

let DIVIDES_FACT = prove_thm(`DIVIDES_FACT`,
  "!m n. 0 < m /\ m <= n ==> m divides (FACT n)",
  REPEAT GEN_TAC THEN REWRITE_TAC[LESS_EQ_EXISTS] THEN
  DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (X_CHOOSE_THEN "d:num" SUBST1_TAC)) THEN
  SPEC_TAC("d:num","d:num") THEN INDUCT_TAC THEN
  REWRITE_TAC[ADD_CLAUSES; FACT] THENL
   [SPEC_TAC("m:num","m:num") THEN INDUCT_TAC THEN
    REWRITE_TAC[FACT; DIVIDES_REFL; LESS_REFL] THEN
    DISCH_TAC THEN MATCH_MP_TAC DIVIDES_RMUL THEN
    MATCH_ACCEPT_TAC DIVIDES_REFL;
    DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
    MATCH_ACCEPT_TAC DIVIDES_LMUL]);;

let DIVIDES_2 = prove_thm(`DIVIDES_2`,
  "!n. 2 divides n = EVEN(n)",
  REWRITE_TAC[divides; EVEN_EXISTS]);;

let DIVIDES_REXP = prove_thm(`DIVIDES_REXP`,
  "!x y n. x divides y ==> x divides (y EXP (SUC n))",
  REWRITE_TAC[EXP; DIVIDES_RMUL]);;

%----------------------------------------------------------------------------%
% The Bezout theorem is a bit ugly for N; it'd be easier for Z               %
%----------------------------------------------------------------------------%

let IND_EUCLID = prove_thm(`IND_EUCLID`,
  "!P. (!a b. P a b = P b a) /\
       (!a. P a 0) /\
       (!a b. P a b ==> P a (a + b)) ==>
         !a b. P a b",
  REPEAT STRIP_TAC THEN
  W(\(asl,w).  SUBGOAL_THEN "!n a b. (a + b = n) ==> ^w" MATCH_MP_TAC) THENL
   [ALL_TAC; EXISTS_TAC "a + b" THEN REFL_TAC] THEN
  COMPLETE_INDUCT_TAC THEN
  REPEAT STRIP_TAC THEN REPEAT_TCL DISJ_CASES_THEN MP_TAC
   (SPECL ["a:num"; "b:num"] LESS_LESS_CASES) THENL
   [DISCH_THEN SUBST1_TAC THEN
    GEN_REWRITE_TAC RAND_CONV [] [GSYM ADD_0] THEN
    FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
    ALL_TAC; ALL_TAC] THEN
  DISCH_THEN(\th. SUBST1_TAC(SYM(MATCH_MP SUB_ADD
   (MATCH_MP LESS_IMP_LESS_OR_EQ th))) THEN
    DISJ_CASES_THEN MP_TAC (MATCH_MP DIFF_LEMMA th)) THENL
   [DISCH_THEN SUBST1_TAC THEN
    FIRST_ASSUM (CONV_TAC o REWR_CONV) THEN
    FIRST_ASSUM MATCH_ACCEPT_TAC;
    REWRITE_TAC[ASSUME "a + b = n"] THEN
    DISCH_TAC THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
    FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM(IMP_RES_THEN MATCH_MP_TAC);
    DISCH_THEN SUBST1_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC;
    REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] (ASSUME "a + b = n")] THEN
    DISCH_TAC THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
    FIRST_ASSUM (CONV_TAC o REWR_CONV) THEN
    FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM(IMP_RES_THEN MATCH_MP_TAC)] THEN
  REWRITE_TAC[]);;

let BEZOUT_LEMMA = prove_thm(`BEZOUT_LEMMA`,
  "!a b. (?d x y. (d divides a /\ d divides b) /\
                  ((a * x = (b * y) + d) \/
                   (b * x = (a * y) + d)))
     ==> (?d x y. (d divides a /\ d divides (a + b)) /\
                  ((a * x = ((a + b) * y) + d) \/
                   ((a + b) * x = (a * y) + d)))",
  REPEAT STRIP_TAC THEN EXISTS_TAC "d:num" THENL
   [MAP_EVERY EXISTS_TAC ["x + y"; "y:num"];
    MAP_EVERY EXISTS_TAC ["x:num"; "x + y"]] THEN
  ASM_REWRITE_TAC[] THEN
  (CONJ_TAC THENL [MATCH_MP_TAC DIVIDES_ADD; ALL_TAC]) THEN
  ASM_REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
  REWRITE_TAC[ADD_ASSOC] THEN DISJ1_TAC THEN
  CONV_TAC(AC_CONV(ADD_ASSOC,ADD_SYM)));;

let BEZOUT_ADD = prove_thm(`BEZOUT_ADD`,
  "!a b. ?d x y. (d divides a /\ d divides b) /\
                 ((a * x = (b * y) + d) \/
                  (b * x = (a * y) + d))",
  W(\(asl,w). MP_TAC(SPEC "\(a:num) (b:num). ^(snd(strip_forall w))"
    IND_EUCLID)) THEN BETA_TAC THEN DISCH_THEN MATCH_MP_TAC THEN
  REPEAT CONJ_TAC THENL
   [REPEAT GEN_TAC THEN REPEAT
     (AP_TERM_TAC THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN BETA_TAC) THEN
    GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [] [DISJ_SYM] THEN
    GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [] [CONJ_SYM] THEN REFL_TAC;
    GEN_TAC THEN MAP_EVERY EXISTS_TAC ["a:num"; "1"; "0"] THEN
    REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; DIVIDES_0; DIVIDES_REFL];
    MATCH_ACCEPT_TAC BEZOUT_LEMMA]);;

let BEZOUT = prove_thm(`BEZOUT`,
  "!a b. ?d x y. (d divides a /\ d divides b) /\
                 (((a * x) - (b * y) = d) \/
                  ((b * x) - (a * y) = d))",
  REPEAT GEN_TAC THEN REPEAT_TCL STRIP_THM_THEN ASSUME_TAC
   (SPECL ["a:num"; "b:num"] BEZOUT_ADD) THEN
  REPEAT(W(EXISTS_TAC o fst o dest_exists o snd)) THEN
  ASM_REWRITE_TAC[] THEN
  ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[ADD_SUB]);;

%----------------------------------------------------------------------------%
% Greatest common divisor.                                                   %
%----------------------------------------------------------------------------%

let gcd = new_definition(`gcd`,
  "gcd(a,b) = @d. (d divides a /\ d divides b) /\
                  (!e. e divides a /\ e divides b ==> e divides d)");;

let GCD = prove_thm(`GCD`,
  "!a b. (gcd(a,b) divides a /\ gcd(a,b) divides b) /\
         (!e. e divides a /\ e divides b ==> e divides gcd(a,b))",
  REPEAT GEN_TAC THEN REWRITE_TAC[gcd] THEN
  CONV_TAC SELECT_CONV THEN MP_TAC(SPECL ["a:num"; "b:num"] BEZOUT) THEN
  DISCH_THEN(EVERY_TCL (map X_CHOOSE_THEN ["d:num"; "x:num"; "y:num"])
    STRIP_ASSUME_TAC) THEN
  EXISTS_TAC "d:num" THEN ASM_REWRITE_TAC[] THEN
  X_GEN_TAC "e:num" THEN STRIP_TAC THEN
  FIRST_ASSUM(UNDISCH_TAC o assert is_eq o concl) THEN
  DISCH_THEN(SUBST1_TAC o SYM) THEN
  MATCH_MP_TAC DIVIDES_SUB THEN CONJ_TAC THEN
  MATCH_MP_TAC DIVIDES_RMUL THEN
  FIRST_ASSUM MATCH_ACCEPT_TAC);;

let GCD_COMMON = prove_thm(`GCD_COMMON`,
  "!d a b. d divides a /\ d divides b = d divides gcd(a,b)",
  REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[GCD] THEN
  DISCH_TAC THEN CONJ_TAC THEN MATCH_MP_TAC DIVIDES_TRANS THEN
  EXISTS_TAC "gcd(a,b)" THEN ASM_REWRITE_TAC[GCD]);;

let GCD_UNIQUE = prove_thm(`GCD_UNIQUE`,
  "!d a b. (d divides a /\ d divides b) /\
           (!e. e divides a /\ e divides b ==> e divides d) =
           (d = gcd(a,b))",
  REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[GCD] THEN
  ONCE_REWRITE_TAC[GSYM DIVIDES_ANTISYM] THEN
  ASM_REWRITE_TAC[GSYM GCD_COMMON] THEN
  FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[GCD]);;

let DIVIDES_GCD = prove_thm(`DIVIDES_GCD`,
  "!a b d. d divides gcd(a,b) = d divides a /\ d divides b",
  REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[GCD] THEN
  DISCH_TAC THEN CONJ_TAC THEN
  MATCH_MP_TAC DIVIDES_TRANS THEN EXISTS_TAC "gcd(a,b)" THEN
  ASM_REWRITE_TAC[GCD]);;

let GCD_SYM = prove_thm(`GCD_SYM`,
  "!a b. gcd(a,b) = gcd(b,a)",
  REPEAT GEN_TAC THEN REWRITE_TAC[gcd] THEN
  AP_TERM_TAC THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN BETA_TAC THEN
  MATCH_MP_TAC(TAUT_CONV "(a = b) /\ (c = d) ==> (a /\ c = b /\ d)") THEN
  CONJ_TAC THEN GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV)
   [] [CONJ_SYM] THEN REFL_TAC);;

let GCD_ASSOC = prove_thm(`GCD_ASSOC`,
  "!a b c. gcd(a,gcd(b,c)) = gcd(gcd(a,b),c)",
  REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM GCD_UNIQUE] THEN
  REWRITE_TAC[DIVIDES_GCD; CONJ_ASSOC; GCD] THEN
  CONJ_TAC THEN MATCH_MP_TAC DIVIDES_TRANS THEN
  EXISTS_TAC "gcd(b,c)" THEN ASM_REWRITE_TAC[GCD]);;

let BEZOUT_GCD = prove_thm(`BEZOUT_GCD`,
  "!a b. ?x y. ((a * x) - (b * y) = gcd(a,b)) \/
               ((b * x) - (a * y) = gcd(a,b))",
  REPEAT GEN_TAC THEN
  MP_TAC(SPECL ["a:num"; "b:num"] BEZOUT) THEN
  DISCH_THEN(EVERY_TCL (map X_CHOOSE_THEN ["d:num"; "x:num"; "y:num"])
    (CONJUNCTS_THEN ASSUME_TAC)) THEN
  SUBGOAL_THEN "d divides gcd(a,b)" MP_TAC THENL
   [MATCH_MP_TAC(last(CONJUNCTS(SPEC_ALL GCD))) THEN ASM_REWRITE_TAC[];
    DISCH_THEN(X_CHOOSE_THEN "k:num" SUBST1_TAC o REWRITE_RULE[divides]) THEN
    MAP_EVERY EXISTS_TAC ["x * k"; "y * k"] THEN
    ASM_REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB; MULT_ASSOC] THEN
    FIRST_ASSUM(DISJ_CASES_THEN SUBST1_TAC) THEN REWRITE_TAC[]]);;

let GCD_LMUL = prove_thm(`GCD_LMUL`,
  "!a b c. gcd(c * a, c * b) = c * gcd(a,b)",
  REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN
  ONCE_REWRITE_TAC[GSYM GCD_UNIQUE] THEN
  REPEAT CONJ_TAC THEN TRY(MATCH_MP_TAC DIVIDES_MUL_L) THEN
  REWRITE_TAC[GCD] THEN REPEAT STRIP_TAC THEN
  REPEAT_TCL STRIP_THM_THEN (SUBST1_TAC o SYM)
   (SPECL ["a:num"; "b:num"] BEZOUT_GCD) THEN
  REWRITE_TAC[LEFT_SUB_DISTRIB; MULT_ASSOC] THEN
  MATCH_MP_TAC DIVIDES_SUB THEN CONJ_TAC THEN
  MATCH_MP_TAC DIVIDES_RMUL THEN ASM_REWRITE_TAC[]);;

let GCD_RMUL = prove_thm(`GCD_RMUL`,
  "!a b c. gcd(a * c, b * c) = c * gcd(a,b)",
  REPEAT GEN_TAC THEN
  GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [] [MULT_SYM] THEN
  MATCH_ACCEPT_TAC GCD_LMUL);;

let GCD_BEZOUT = prove_thm(`GCD_BEZOUT`,
  "!a b d. (?x y. ((a * x) - (b * y) = d) \/ ((b * x) - (a * y) = d)) =
           gcd(a,b) divides d",
  REPEAT GEN_TAC THEN EQ_TAC THENL
   [STRIP_TAC THEN POP_ASSUM(SUBST1_TAC o SYM) THEN
    MATCH_MP_TAC DIVIDES_SUB THEN CONJ_TAC THEN
    MATCH_MP_TAC DIVIDES_RMUL THEN REWRITE_TAC[GCD];
    DISCH_THEN(X_CHOOSE_THEN "k:num" SUBST1_TAC o REWRITE_RULE[divides]) THEN
    STRIP_ASSUME_TAC(SPECL ["a:num"; "b:num"] BEZOUT_GCD) THEN
    MAP_EVERY EXISTS_TAC ["x * k"; "y * k"] THEN
    ASM_REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB; MULT_ASSOC] THEN
    FIRST_ASSUM(DISJ_CASES_THEN SUBST1_TAC) THEN REWRITE_TAC[]]);;

let GCD_BEZOUT_SUM = prove_thm(`GCD_BEZOUT_SUM`,
  "!a b d x y. ((a * x) + (b * y) = d) ==> gcd(a,b) divides d",
  REPEAT GEN_TAC THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
  MATCH_MP_TAC DIVIDES_ADD THEN CONJ_TAC THEN
  MATCH_MP_TAC DIVIDES_RMUL THEN REWRITE_TAC[GCD]);;

let GCD_0 = prove_thm(`GCD_0`,
  "!a. gcd(0,a) = a",
  GEN_TAC THEN CONV_TAC SYM_CONV THEN
  REWRITE_TAC[GSYM GCD_UNIQUE] THEN
  REWRITE_TAC[DIVIDES_0; DIVIDES_REFL] THEN
  REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);;

let GCD_ZERO = prove_thm(`GCD_ZERO`,
  "!a b. (gcd(a,b) = 0) = (a = 0) /\ (b = 0)",
  REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN
  ASM_REWRITE_TAC[GCD_0] THEN
  MP_TAC(SPECL ["a:num"; "b:num"] GCD) THEN
  ASM_REWRITE_TAC[DIVIDES_ZERO] THEN
  STRIP_TAC THEN ASM_REWRITE_TAC[]);;

let GCD_REFL = prove_thm(`GCD_REFL`,
  "!a. gcd(a,a) = a",
  GEN_TAC THEN CONV_TAC SYM_CONV THEN
  ONCE_REWRITE_TAC[GSYM GCD_UNIQUE] THEN
  REWRITE_TAC[DIVIDES_REFL]);;

let GCD_1 = prove_thm(`GCD_1`,
  "!a. gcd(1,a) = 1",
  GEN_TAC THEN CONV_TAC SYM_CONV THEN
  ONCE_REWRITE_TAC[GSYM GCD_UNIQUE] THEN
  REWRITE_TAC[DIVIDES_1] THEN
  REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[]);;

let GCD_MULTIPLE = prove_thm(`GCD_MULTIPLE`,
  "!a b. gcd(b,a * b) = b",
  REPEAT GEN_TAC THEN
  GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV)
   [] [SYM(el 3 (CONJUNCTS(SPEC_ALL MULT_CLAUSES)))] THEN
  REWRITE_TAC[GCD_RMUL; GCD_1] THEN
  REWRITE_TAC[MULT_CLAUSES]);;

%----------------------------------------------------------------------------%
% Coprimality                                                                %
%----------------------------------------------------------------------------%

let coprime = new_definition(`coprime`,
  "coprime(a,b) = !d. d divides a /\ d divides b ==> (d = 1)");;

let COPRIME = prove_thm(`COPRIME`,
  "!a b. coprime(a,b) = !d. d divides a /\ d divides b = (d = 1)",
  REPEAT GEN_TAC THEN REWRITE_TAC[coprime] THEN
  REPEAT(EQ_TAC ORELSE STRIP_TAC) THEN ASM_REWRITE_TAC[DIVIDES_1] THENL
   [FIRST_ASSUM MATCH_MP_TAC;
    FIRST_ASSUM(CONV_TAC o REWR_CONV o GSYM) THEN CONJ_TAC] THEN
  ASM_REWRITE_TAC[]);;

let COPRIME_GCD = prove_thm(`COPRIME_GCD`,
  "!a b. coprime(a,b) = (gcd(a,b) = 1)",
  REPEAT GEN_TAC THEN REWRITE_TAC[coprime] THEN EQ_TAC THENL
   [DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[GCD];
    DISCH_TAC THEN MP_TAC(SPECL ["a:num"; "b:num"] GCD) THEN
    ASM_REWRITE_TAC[DIVIDES_ONE] THEN DISCH_THEN(\th. REWRITE_TAC[th])]);;

let COPRIME_SYM = prove_thm(`COPRIME_SYM`,
  "!a b. coprime(a,b) = coprime(b,a)",
  REPEAT GEN_TAC THEN REWRITE_TAC[COPRIME_GCD] THEN
  AP_THM_TAC THEN AP_TERM_TAC THEN
  MATCH_ACCEPT_TAC GCD_SYM);;

let COPRIME_BEZOUT = prove_thm(`COPRIME_BEZOUT`,
  "!a b. coprime(a,b) = ?x y. ((a * x) - (b * y) = 1) \/
                              ((b * x) - (a * y) = 1)",
  REWRITE_TAC[GCD_BEZOUT; DIVIDES_ONE; COPRIME_GCD]);;

let COPRIME_DIVPROD = prove_thm(`COPRIME_DIVPROD`,
  "!d a b. d divides (a * b) /\ coprime(d,a) ==> d divides b",
  REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  REWRITE_TAC[COPRIME_BEZOUT] THEN
  DISCH_THEN(X_CHOOSE_THEN "x:num" MP_TAC) THEN
  DISCH_THEN(X_CHOOSE_THEN "y:num" MP_TAC) THEN
  DISCH_THEN (DISJ_CASES_THEN (MP_TAC o AP_TERM "$* b")) THEN
  REWRITE_TAC[MULT_CLAUSES] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
  REWRITE_TAC[LEFT_SUB_DISTRIB; MULT_ASSOC] THEN
  MATCH_MP_TAC DIVIDES_SUB THEN CONJ_TAC THEN
  MATCH_MP_TAC DIVIDES_RMUL THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
  ASM_REWRITE_TAC[] THEN MATCH_MP_TAC DIVIDES_RMUL THEN
  ASM_REWRITE_TAC[DIVIDES_REFL]);;

let COPRIME_1 = prove_thm(`COPRIME_1`,
  "!a. coprime(a,1)",
  GEN_TAC THEN REWRITE_TAC[coprime; DIVIDES_ONE] THEN
  GEN_TAC THEN DISCH_THEN(\th. REWRITE_TAC[th]));;

let GCD_COPRIME = prove_thm(`GCD_COPRIME`,
  "!a b a' b'. ~(gcd(a,b) = 0) /\
               (a = a' * gcd(a,b)) /\
               (b = b' * gcd(a,b)) ==> coprime(a',b')",
  REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[coprime] THEN
  CONV_TAC (ONCE_DEPTH_CONV NOT_FORALL_CONV) THEN
  REWRITE_TAC[NOT_IMP] THEN DISCH_THEN(X_CHOOSE_TAC "d:num") THEN
  POP_ASSUM(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
  REWRITE_TAC[divides] THEN
  DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN "a'':num" SUBST1_TAC)
    (X_CHOOSE_THEN "b'':num" SUBST1_TAC)) THEN
  ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[MULT_ASSOC] THEN
  DISCH_TAC THEN MP_TAC(SPECL ["a:num"; "b:num"] GCD) THEN
  DISCH_THEN(MP_TAC o SPEC "gcd(a,b) * d" o last o CONJUNCTS) THEN
  REWRITE_TAC[NOT_IMP] THEN REPEAT CONJ_TAC THENL
   [REWRITE_TAC[divides] THEN EXISTS_TAC "a'':num" THEN
    FIRST_ASSUM(MATCH_ACCEPT_TAC o CONJUNCT1);
    REWRITE_TAC[divides] THEN EXISTS_TAC "b'':num" THEN
    FIRST_ASSUM(MATCH_ACCEPT_TAC o CONJUNCT2);
    DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN
    REWRITE_TAC[DE_MORGAN_THM; NOT_LESS_EQUAL] THEN
    FIRST_ASSUM(UNDISCH_TAC o assert is_conj o concl) THEN
    UNDISCH_TAC "~(d = 1)" THEN
    STRUCT_CASES_TAC(SPEC "d:num" num_CASES) THEN
    REWRITE_TAC[MULT_CLAUSES; SUC_NOT; num_CONV "1"; INV_SUC_EQ] THENL
     [DISCH_THEN(CONJUNCTS_THEN SUBST_ALL_TAC) THEN
      POP_ASSUM MP_TAC THEN REWRITE_TAC[GCD_0];
      DISCH_TAC THEN DISCH_THEN(K ALL_TAC) THEN
      ASM_REWRITE_TAC[] THEN MATCH_MP_TAC LESS_ADD_NONZERO THEN
      ASM_REWRITE_TAC[MULT_EQ_0]]]);;

let GCD_COPRIME_EXISTS = prove_thm(`GCD_COPRIME_EXISTS`,
  "!a b. ~(gcd(a,b) = 0) ==>
        ?a' b'. (a = a' * gcd(a,b)) /\
                (b = b' * gcd(a,b)) /\
                coprime(a',b')",
  REPEAT GEN_TAC THEN DISCH_TAC THEN MP_TAC(SPECL ["a:num"; "b:num"] GCD) THEN
  DISCH_THEN(MP_TAC o CONJUNCT1) THEN REWRITE_TAC[divides] THEN
  DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC "a':num" o GSYM)
   (X_CHOOSE_TAC "b':num" o GSYM)) THEN
  MAP_EVERY EXISTS_TAC ["a':num"; "b':num"] THEN
  ONCE_REWRITE_TAC[MULT_SYM] THEN ASM_REWRITE_TAC[] THEN
  MATCH_MP_TAC GCD_COPRIME THEN
  MAP_EVERY EXISTS_TAC ["a:num"; "b:num"] THEN
  ONCE_REWRITE_TAC[MULT_SYM] THEN ASM_REWRITE_TAC[]);;

let COPRIME_0 = prove_thm(`COPRIME_0`,
  "!d. coprime(d,0) = (d = 1)",
  GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN
  ASM_REWRITE_TAC[ONCE_REWRITE_RULE[COPRIME_SYM] COPRIME_1] THEN
  POP_ASSUM MP_TAC THEN REWRITE_TAC[coprime] THEN
  DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[DIVIDES_REFL; DIVIDES_0]);;

let COPRIME_MUL = prove_thm(`COPRIME_MUL`,
  "!d a b. coprime(d,a) /\ coprime(d,b) ==> coprime(d,a * b)",
  REPEAT GEN_TAC THEN REWRITE_TAC[COPRIME_GCD] THEN
  DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (MP_TAC o AP_TERM "$* a")) THEN
  REWRITE_TAC[MULT_CLAUSES] THEN DISCH_THEN
   (\th. GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [] [GSYM th]) THEN
  REWRITE_TAC[GSYM GCD_LMUL; GCD_ASSOC; GCD_MULTIPLE]);;

let COPRIME_LMUL2 = prove_thm(`COPRIME_LMUL2`,
  "!d a b. coprime(d,a * b) ==> coprime(d,b)",
  REPEAT GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN
  REWRITE_TAC[coprime] THEN CONV_TAC(ONCE_DEPTH_CONV NOT_FORALL_CONV) THEN
  REWRITE_TAC[NOT_IMP] THEN
  DISCH_THEN(X_CHOOSE_THEN "k:num" STRIP_ASSUME_TAC) THEN
  EXISTS_TAC "k:num" THEN ASM_REWRITE_TAC[] THEN
  MATCH_MP_TAC DIVIDES_LMUL THEN ASM_REWRITE_TAC[]);;

let COPRIME_RMUL2 = prove_thm(`COPRIME_RMUL2`,
  "!d a b.  coprime(d,a * b) ==> coprime(d,a)",
  ONCE_REWRITE_TAC[MULT_SYM] THEN REWRITE_TAC[COPRIME_LMUL2]);;

let COPRIME_EXP = prove_thm(`COPRIME_EXP`,
  "!n a d. coprime(d,a) ==> coprime(d,a EXP n)",
  INDUCT_TAC THEN REWRITE_TAC[EXP; COPRIME_1] THEN
  REPEAT GEN_TAC THEN DISCH_TAC THEN
  MATCH_MP_TAC COPRIME_MUL THEN ASM_REWRITE_TAC[] THEN
  FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;

let COPRIME_EXP_IMP = prove_thm(`COPRIME_EXP_IMP`,
  "!n a b. coprime(a,b) ==> coprime(a EXP n,b EXP n)",
  REPEAT GEN_TAC THEN DISCH_TAC THEN
  MATCH_MP_TAC COPRIME_EXP THEN ONCE_REWRITE_TAC[COPRIME_SYM] THEN
  MATCH_MP_TAC COPRIME_EXP THEN
  ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_REWRITE_TAC[]);;

let BEZOUT_GCD_POW = prove_thm(`BEZOUT_GCD_POW`,
  "!n a b. ?x y. (((a EXP n) * x) - ((b EXP n) * y) = gcd(a,b) EXP n) \/
                 (((b EXP n) * x) - ((a EXP n) * y) = gcd(a,b) EXP n)",
  REPEAT GEN_TAC THEN ASM_CASES_TAC "gcd(a,b) = 0" THENL
   [STRUCT_CASES_TAC(SPEC "n:num" num_CASES) THEN
    ASM_REWRITE_TAC[EXP; MULT_CLAUSES] THENL
     [MAP_EVERY EXISTS_TAC ["1"; "0"] THEN REWRITE_TAC[SUB_0];
      REPEAT(EXISTS_TAC "0") THEN REWRITE_TAC[MULT_CLAUSES; SUB_0]];
    MP_TAC(SPECL ["a:num"; "b:num"] GCD) THEN
    DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
    DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN REWRITE_TAC[divides] THEN
    DISCH_THEN(X_CHOOSE_THEN "b':num" ASSUME_TAC) THEN
    DISCH_THEN(X_CHOOSE_THEN "a':num" ASSUME_TAC) THEN
    MP_TAC(SPECL ["a:num"; "b:num"; "a':num"; "b':num"] GCD_COPRIME) THEN
    RULE_ASSUM_TAC GSYM THEN RULE_ASSUM_TAC(ONCE_REWRITE_RULE[MULT_SYM]) THEN
    ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o GSYM) THEN
    ASM_REWRITE_TAC[] THEN
    DISCH_THEN(MP_TAC o SPEC "n:num" o MATCH_MP COPRIME_EXP_IMP) THEN
    REWRITE_TAC[COPRIME_BEZOUT] THEN
    DISCH_THEN(X_CHOOSE_THEN "x:num" (X_CHOOSE_THEN "y:num" MP_TAC)) THEN
    DISCH_THEN(DISJ_CASES_THEN MP_TAC) THEN
    DISCH_THEN (MP_TAC o AP_TERM "$* (gcd(a,b) EXP n)") THEN
    REWRITE_TAC[MULT_CLAUSES; LEFT_SUB_DISTRIB] THEN
    DISCH_THEN(SUBST1_TAC o SYM) THEN
    MAP_EVERY EXISTS_TAC ["x:num"; "y:num"] THEN
    REWRITE_TAC[MULT_ASSOC; GSYM MULT_EXP] THEN
    RULE_ASSUM_TAC(ONCE_REWRITE_RULE[MULT_SYM]) THEN
    ASM_REWRITE_TAC[]]);;

let GCD_EXP = prove_thm(`GCD_EXP`,
  "!n a b. gcd(a EXP n,b EXP n) = gcd(a,b) EXP n",
  REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN
  ONCE_REWRITE_TAC[GSYM GCD_UNIQUE] THEN REPEAT CONJ_TAC THENL
   [MATCH_MP_TAC DIVIDES_EXP THEN REWRITE_TAC[GCD];
    MATCH_MP_TAC DIVIDES_EXP THEN REWRITE_TAC[GCD];
    X_GEN_TAC "d:num" THEN STRIP_TAC THEN
    MP_TAC(SPECL ["n:num"; "a:num"; "b:num"] BEZOUT_GCD_POW) THEN
    DISCH_THEN(REPEAT_TCL CHOOSE_THEN (DISJ_CASES_THEN
     (SUBST1_TAC o SYM))) THEN
    MATCH_MP_TAC DIVIDES_SUB THEN CONJ_TAC THEN
    MATCH_MP_TAC DIVIDES_RMUL THEN ASM_REWRITE_TAC[]]);;

let COPRIME_EXP2 = prove_thm(`COPRIME_EXP2`,
  "!n a b. coprime(a EXP (SUC n),b EXP (SUC n)) = coprime(a,b)",
  REWRITE_TAC[COPRIME_GCD; GCD_EXP] THEN
  INDUCT_TAC THEN ONCE_REWRITE_TAC[EXP] THENL
   [REWRITE_TAC[EXP; MULT_CLAUSES];
    ASM_REWRITE_TAC[MULT_EQ_1]]);;

let DIVISION_DECOMP = prove_thm(`DIVISION_DECOMP`,
  "!a b c. a divides (b * c) ==>
     ?b' c'. (a = b' * c') /\ b' divides b /\ c' divides c",
  REPEAT GEN_TAC THEN DISCH_TAC THEN
  EXISTS_TAC "gcd(a,b)" THEN REWRITE_TAC[GCD] THEN
  MP_TAC(SPECL ["a:num"; "b:num"] GCD_COPRIME_EXISTS) THEN
  ASM_CASES_TAC "gcd(a,b) = 0" THENL
   [ASM_REWRITE_TAC[] THEN EXISTS_TAC "1" THEN
    RULE_ASSUM_TAC(REWRITE_RULE[GCD_ZERO]) THEN
    ASM_REWRITE_TAC[MULT_CLAUSES; DIVIDES_1];
    ASM_REWRITE_TAC[] THEN
    DISCH_THEN(X_CHOOSE_THEN "a':num" (X_CHOOSE_THEN "b':num"
      (STRIP_ASSUME_TAC o GSYM o ONCE_REWRITE_RULE[MULT_SYM]))) THEN
    EXISTS_TAC "a':num" THEN ASM_REWRITE_TAC[] THEN
    UNDISCH_TAC "a divides (b * c)" THEN
    FIRST_ASSUM(\th. GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [] [GSYM th]) THEN
    FIRST_ASSUM(\th. GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV)
     [] [GSYM th]) THEN REWRITE_TAC[MULT_ASSOC] THEN
    DISCH_TAC THEN MATCH_MP_TAC COPRIME_DIVPROD THEN
    EXISTS_TAC "b':num" THEN ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC DIVIDES_CMUL2 THEN EXISTS_TAC "gcd(a,b)" THEN
    REWRITE_TAC[MULT_ASSOC] THEN CONJ_TAC THEN
    FIRST_ASSUM MATCH_ACCEPT_TAC]);;

let DIVIDES_REV = prove_thm(`DIVIDES_REV`,
  "!n a b. (a EXP n) divides (b EXP n) /\ ~(n = 0) ==> a divides b",
  REPEAT GEN_TAC THEN STRIP_TAC THEN
  ASM_CASES_TAC "gcd(a,b) = 0" THENL
   [RULE_ASSUM_TAC(REWRITE_RULE[GCD_ZERO]) THEN
    ASM_REWRITE_TAC[DIVIDES_REFL]; ALL_TAC] THEN
  FIRST_ASSUM(MP_TAC o MATCH_MP GCD_COPRIME_EXISTS) THEN
  DISCH_THEN(X_CHOOSE_THEN "a':num" (X_CHOOSE_THEN "b':num"
   (STRIP_ASSUME_TAC o GSYM))) THEN
  UNDISCH_TAC "(a EXP n) divides (b EXP n)" THEN
  DISCH_THEN(X_CHOOSE_THEN "k:num" MP_TAC o REWRITE_RULE[divides]) THEN
  FIRST_ASSUM(\th. GEN_REWRITE_TAC (funpow 3 LAND_CONV) [] [GSYM th]) THEN
  FIRST_ASSUM(\th. GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o
    LAND_CONV o LAND_CONV) [] [GSYM th]) THEN
  REWRITE_TAC[SPECL ["x:num"; "gcd(a,b)"] MULT_SYM] THEN
  REWRITE_TAC[MULT_EXP; GSYM MULT_ASSOC] THEN
  SUBGOAL_THEN "~(gcd(a,b) EXP n = 0)" MP_TAC THENL
   [UNDISCH_TAC "~(gcd(a,b) = 0)" THEN
    STRUCT_CASES_TAC(SPEC "gcd(a,b)" num_CASES) THEN
    REWRITE_TAC[NOT_EXP_0];
    ONCE_REWRITE_TAC[TAUT_CONV "a ==> b ==> c = a /\ b ==> c"]] THEN
  DISCH_THEN(MP_TAC o MATCH_MP MULT_LCANCEL) THEN
  DISCH_TAC THEN SUBGOAL_THEN "coprime(a' EXP n,b' EXP n)" MP_TAC THENL
   [UNDISCH_TAC "~(n = 0)" THEN
    STRUCT_CASES_TAC(SPEC "n:num" num_CASES) THEN
    ASM_REWRITE_TAC[COPRIME_EXP2]; ALL_TAC] THEN
  ASM_REWRITE_TAC[coprime] THEN
  DISCH_THEN(MP_TAC o SPEC "a' EXP n") THEN
  REWRITE_TAC[MATCH_MP DIVIDES_RMUL (SPEC_ALL DIVIDES_REFL); DIVIDES_REFL] THEN
  ASM_REWRITE_TAC[EXP_EQ_1] THEN DISCH_THEN SUBST_ALL_TAC THEN
  UNDISCH_TAC "1 * gcd(a,b) = a" THEN REWRITE_TAC[MULT_CLAUSES] THEN
  DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[GCD]);;

let DIVIDES_MUL = prove_thm(`DIVIDES_MUL`,
  "!m n r. m divides r /\ n divides r /\ coprime(m,n) ==> (m * n) divides r",
  REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  POP_ASSUM(X_CHOOSE_THEN "d:num" SUBST1_TAC o REWRITE_RULE[divides]) THEN
  ONCE_REWRITE_TAC[COPRIME_SYM] THEN
  DISCH_THEN(MP_TAC o MATCH_MP COPRIME_DIVPROD) THEN
  MATCH_ACCEPT_TAC DIVIDES_MUL_L);;

%----------------------------------------------------------------------------%
% Primality                                                                  %
%----------------------------------------------------------------------------%

let prime = new_definition(`prime`,
  "prime(p) = ~(p = 1) /\ !x. x divides p ==> (x = 1) \/ (x = p)");;

%----------------------------------------------------------------------------%
% A few useful theorems about primes                                         %
%----------------------------------------------------------------------------%

let PRIME_0 = prove_thm(`PRIME_0`,
  "~prime(0)",
  REWRITE_TAC[prime] THEN
  DISCH_THEN(MP_TAC o SPEC "2" o CONJUNCT2) THEN
  REWRITE_TAC[DIVIDES_0] THEN REDUCE_TAC);;

let PRIME_1 = prove_thm(`PRIME_1`,
  "~prime(1)",
  REWRITE_TAC[prime]);;

let PRIME_2 = prove_thm(`PRIME_2`,
  "prime(2)",
  REWRITE_TAC[prime] THEN REDUCE_TAC THEN
  REWRITE_TAC[] THEN REPEAT STRIP_TAC THEN
  FIRST_ASSUM(MP_TAC o MATCH_MP DIVIDES_LE) THEN
  REDUCE_TAC THEN REWRITE_TAC[LESS_OR_EQ] THEN
  REWRITE_TAC[num_CONV "2"; num_CONV "1"; LESS_THM; NOT_LESS_0] THEN
  DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN SUBST_ALL_TAC) THEN
  REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[DIVIDES_ZERO] THEN
  REDUCE_TAC THEN REWRITE_TAC[]);;

let PRIME_GE_2 = prove_thm(`PRIME_GE_2`,
  "!p. prime(p) ==> 2 <= p",
  GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[NOT_LESS_EQUAL] THEN
  REWRITE_TAC[num_CONV "2"; num_CONV "1"; LESS_THM; NOT_LESS_0] THEN
  DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN SUBST1_TAC) THEN
  REWRITE_TAC[SYM(num_CONV "1"); PRIME_0; PRIME_1]);;

let PRIME_FACTOR = prove_thm(`PRIME_FACTOR`,
  "!n. ~(n = 1) ==> ?p. prime(p) /\ p divides n",
  COMPLETE_INDUCT_TAC THEN
  X_GEN_TAC "n:num" THEN REPEAT STRIP_TAC THEN
  ASM_CASES_TAC "prime(n)" THENL
   [EXISTS_TAC "n:num" THEN ASM_REWRITE_TAC[DIVIDES_REFL];
    UNDISCH_TAC "~prime(n)" THEN
    DISCH_THEN(MP_TAC o REWRITE_RULE[prime]) THEN
    ASM_REWRITE_TAC[] THEN CONV_TAC(ONCE_DEPTH_CONV NOT_FORALL_CONV) THEN
    DISCH_THEN(X_CHOOSE_THEN "m:num" MP_TAC) THEN
    REWRITE_TAC[NOT_IMP; DE_MORGAN_THM] THEN STRIP_TAC THEN
    FIRST_ASSUM(DISJ_CASES_THEN MP_TAC o MATCH_MP DIVIDES_LE) THENL
     [ASM_REWRITE_TAC[LESS_OR_EQ] THEN
      DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN ASM_REWRITE_TAC[] THEN
      DISCH_THEN(X_CHOOSE_THEN "p:num" STRIP_ASSUME_TAC) THEN
      EXISTS_TAC "p:num" THEN ASM_REWRITE_TAC[] THEN
      MATCH_MP_TAC DIVIDES_TRANS THEN EXISTS_TAC "m:num" THEN
      ASM_REWRITE_TAC[];
      DISCH_THEN SUBST1_TAC THEN EXISTS_TAC "2" THEN
      REWRITE_TAC[PRIME_2; DIVIDES_0]]]);;

let PRIME_FACTOR_LT = prove_thm(`PRIME_FACTOR_LT`,
  "!n m p. prime(p) /\ ~(n = 0) /\ (n = p * m) ==> m < n",
  REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_GE_2) THEN
  ASM_REWRITE_TAC[LESS_EQ_EXISTS] THEN
  DISCH_THEN(X_CHOOSE_THEN "q:num" SUBST_ALL_TAC) THEN
  REWRITE_TAC[num_CONV "2"; RIGHT_ADD_DISTRIB; MULT_CLAUSES] THEN
  REWRITE_TAC[GSYM ADD_ASSOC] THEN MATCH_MP_TAC LESS_ADD_NONZERO THEN
  REWRITE_TAC[ADD_EQ_0] THEN DISCH_THEN(CONJUNCTS_THEN SUBST_ALL_TAC) THEN
  FIRST_ASSUM(UNDISCH_TAC o assert is_eq o concl) THEN
  ASM_REWRITE_TAC[MULT_CLAUSES]);;

let EUCLID = prove_thm(`EUCLID`,
  "!n. ?p. prime(p) /\ p > n",
  GEN_REWRITE_TAC I [] [TAUT_CONV "x = ~~x"] THEN
  DISCH_THEN(X_CHOOSE_THEN "n:num" MP_TAC o CONV_RULE NOT_FORALL_CONV) THEN
  DISCH_THEN(STRIP_ASSUME_TAC o CONV_RULE NOT_EXISTS_CONV) THEN
  MP_TAC(SPEC "SUC(FACT n)" PRIME_FACTOR) THEN
  REWRITE_TAC[num_CONV "1"; INV_SUC_EQ; GSYM LESS_EQ_0; NOT_LESS_EQUAL;
    FACT_LESS] THEN DISCH_THEN(X_CHOOSE_TAC "p:num") THEN
  FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) THEN
  DISCH_THEN(MP_TAC o SPEC "p:num") THEN ASM_REWRITE_TAC[] THEN
  DISJ_CASES_TAC(SPECL ["n:num"; "p:num"] LESS_CASES) THEN
  ASM_REWRITE_TAC[GREATER] THEN
  SUBGOAL_THEN "p divides (FACT n)" ASSUME_TAC THENL
   [MATCH_MP_TAC DIVIDES_FACT THEN ASM_REWRITE_TAC[] THEN
    REWRITE_TAC[GSYM NOT_LESS_EQUAL; LESS_EQ_0] THEN
    DISCH_THEN SUBST_ALL_TAC THEN
    EVERY_ASSUM(UNDISCH_TAC o concl) THEN REWRITE_TAC[PRIME_0];
    SUBGOAL_THEN "p = 1" SUBST_ALL_TAC THENL
     [REWRITE_TAC[GSYM DIVIDES_ONE] THEN MATCH_MP_TAC DIVIDES_ADD_REVR THEN
      EXISTS_TAC "FACT n" THEN ASM_REWRITE_TAC[GSYM ADD1];
      FIRST_ASSUM(MP_TAC o CONJUNCT1) THEN REWRITE_TAC[PRIME_1]]]);;

let PRIME_COPRIME = prove_thm(`PRIME_COPRIME`,
  "!n p. prime(p) ==> (n = 1) \/ p divides n \/ coprime(p,n)",
  REPEAT GEN_TAC THEN REWRITE_TAC[prime; COPRIME_GCD] THEN
  STRIP_ASSUME_TAC(SPECL ["p:num"; "n:num"] GCD) THEN
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  DISCH_THEN(MP_TAC o SPEC "gcd(p,n)") THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(DISJ_CASES_THEN SUBST_ALL_TAC) THEN
  ASM_REWRITE_TAC[]);;

let COPRIME_PRIME = prove_thm(`COPRIME_PRIME`,
  "!p a b. coprime(a,b) ==> ~(prime(p) /\ p divides a /\ p divides b)",
  REPEAT GEN_TAC THEN REWRITE_TAC[coprime] THEN REPEAT STRIP_TAC THEN
  SUBGOAL_THEN "p = 1" SUBST_ALL_TAC THENL
   [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
    UNDISCH_TAC "prime 1" THEN REWRITE_TAC[PRIME_1]]);;

let COPRIME_PRIME_EQ = prove_thm(`COPRIME_PRIME_EQ`,
  "!a b. coprime(a,b) = !p. ~(prime(p) /\ p divides a /\ p divides b)",
  REPEAT GEN_TAC THEN EQ_TAC THENL
   [DISCH_THEN(\th. REWRITE_TAC[MATCH_MP COPRIME_PRIME th]);
    CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[coprime] THEN
    CONV_TAC(ONCE_DEPTH_CONV NOT_FORALL_CONV) THEN REWRITE_TAC[NOT_IMP] THEN
    DISCH_THEN(X_CHOOSE_THEN "d:num" STRIP_ASSUME_TAC) THEN
    FIRST_ASSUM(X_CHOOSE_TAC "p:num" o MATCH_MP PRIME_FACTOR) THEN
    EXISTS_TAC "p:num" THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THEN
    MATCH_MP_TAC DIVIDES_TRANS THEN EXISTS_TAC "d:num" THEN
    ASM_REWRITE_TAC[]]);;

let PRIME_DIVPROD = prove_thm(`PRIME_DIVPROD`,
  "!p a b. prime(p) /\ p divides (a * b) ==> p divides a \/ p divides b",
  REPEAT GEN_TAC THEN STRIP_TAC THEN
  FIRST_ASSUM(MP_TAC o SPEC "a:num" o MATCH_MP PRIME_COPRIME) THEN
  DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC) THEN
  ASM_REWRITE_TAC[] THENL
   [DISJ2_TAC THEN UNDISCH_TAC "p divides (a * b)" THEN
    ASM_REWRITE_TAC[MULT_CLAUSES];
    DISJ2_TAC THEN MATCH_MP_TAC COPRIME_DIVPROD THEN
    EXISTS_TAC "a:num" THEN ASM_REWRITE_TAC[]]);;

let PRIME_DIVEXP = prove_thm(`PRIME_DIVEXP`,
  "!n p x. prime(p) /\ p divides (x EXP n) ==> p divides x",
  INDUCT_TAC THEN REPEAT GEN_TAC THEN REWRITE_TAC[EXP; DIVIDES_ONE] THENL
   [DISCH_THEN(SUBST1_TAC o CONJUNCT2) THEN REWRITE_TAC[DIVIDES_1];
    DISCH_THEN(\th. ASSUME_TAC(CONJUNCT1 th) THEN MP_TAC th) THEN
    DISCH_THEN(DISJ_CASES_TAC o MATCH_MP PRIME_DIVPROD) THEN
    ASM_REWRITE_TAC[] THEN FIRST_ASSUM MATCH_MP_TAC THEN
    ASM_REWRITE_TAC[]]);;

let PRIME_DIVEXP_N = prove_thm(`PRIME_DIVEXP_N`,
  "!n p x. prime(p) /\ p divides (x EXP n) ==> (p EXP n) divides (x EXP n)",
  REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP PRIME_DIVEXP) THEN
  MATCH_ACCEPT_TAC DIVIDES_EXP);;

let PARITY_EXP = prove_thm(`PARITY_EXP`,
  "!n x. EVEN(x EXP (SUC n)) = EVEN(x)",
  REPEAT GEN_TAC THEN REWRITE_TAC[GSYM DIVIDES_2] THEN EQ_TAC THENL
   [DISCH_TAC THEN MATCH_MP_TAC PRIME_DIVEXP THEN
    EXISTS_TAC "SUC n" THEN ASM_REWRITE_TAC[PRIME_2];
    REWRITE_TAC[EXP] THEN MATCH_ACCEPT_TAC DIVIDES_RMUL]);;

let COPRIME_SOS = prove_thm(`COPRIME_SOS`,
  "!x y. coprime(x,y) ==> coprime(x * y,(x EXP 2) + (y EXP 2))",
  REPEAT GEN_TAC THEN REWRITE_TAC[COPRIME_PRIME_EQ] THEN
  CONV_TAC CONTRAPOS_CONV THEN
  CONV_TAC(ONCE_DEPTH_CONV NOT_FORALL_CONV) THEN
  REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN "p:num" STRIP_ASSUME_TAC) THEN
  EXISTS_TAC "p:num" THEN ASM_REWRITE_TAC[] THEN
  MP_TAC(SPECL ["p:num"; "x:num"; "y:num"] PRIME_DIVPROD) THEN
  ASM_REWRITE_TAC[] THEN DISCH_THEN DISJ_CASES_TAC THEN
  ASM_REWRITE_TAC[] THEN MATCH_MP_TAC PRIME_DIVEXP THEN
  EXISTS_TAC "2" THEN ASM_REWRITE_TAC[] THEN
  MATCH_MP_TAC DIVIDES_ADD_REVR THENL
   [EXISTS_TAC "x EXP 2";
    EXISTS_TAC "y EXP 2" THEN ONCE_REWRITE_TAC[ADD_SYM]] THEN
  ASM_REWRITE_TAC[] THEN REWRITE_TAC[num_CONV "2"] THEN
  MATCH_MP_TAC DIVIDES_REXP THEN ASM_REWRITE_TAC[]);;

%----------------------------------------------------------------------------%
% One property of coprimality is easier to prove via prime factors.          %
%----------------------------------------------------------------------------%

let PRIME_DIVPROD_POW = prove_thm(`PRIME_DIVPROD_POW`,
  "!n p a b. prime(p) /\ coprime(a,b) /\ (p EXP n) divides (a * b)
                ==> (p EXP n) divides a \/ (p EXP n) divides b",
  REPEAT STRIP_TAC THEN
  ASM_CASES_TAC "n = 0" THEN ASM_REWRITE_TAC[EXP; DIVIDES_1] THEN
  SUBGOAL_THEN "p divides a \/ p divides b" DISJ_CASES_TAC THENL
   [MATCH_MP_TAC PRIME_DIVPROD THEN ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC DIVIDES_EXP2 THEN EXISTS_TAC "n:num" THEN ASM_REWRITE_TAC[];
    DISJ1_TAC THEN RULE_ASSUM_TAC(ONCE_REWRITE_RULE[COPRIME_SYM; MULT_SYM]);
    DISJ2_TAC] THEN
  MATCH_MP_TAC COPRIME_DIVPROD THENL
   [EXISTS_TAC "b:num"; EXISTS_TAC "a:num"] THEN
  ASM_REWRITE_TAC[] THEN
  ONCE_REWRITE_TAC[COPRIME_SYM] THEN
  MATCH_MP_TAC COPRIME_EXP THEN
  FIRST_ASSUM(MP_TAC o SPEC "p:num" o MATCH_MP COPRIME_PRIME) THEN
  ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[COPRIME_SYM] THENL
   [FIRST_ASSUM(MP_TAC o SPEC "b:num" o MATCH_MP PRIME_COPRIME);
    FIRST_ASSUM(MP_TAC o SPEC "a:num" o MATCH_MP PRIME_COPRIME)] THEN
  DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC) THEN
  ASM_REWRITE_TAC[COPRIME_1]);;

let COPRIME_POW = prove_thm(`COPRIME_POW`,
  "!n a b c. coprime(a,b) /\ (a * b = c EXP n) ==>
             ?r s. (a = r EXP n) /\ (b = s EXP n)",
  REPEAT GEN_TAC THEN
  MAP_EVERY (W(curry SPEC_TAC)) ["a:num"; "b:num"; "n:num"; "c:num"] THEN
  COMPLETE_INDUCT_TAC THEN X_GEN_TAC "c:num" THEN
  DISCH_THEN(MP_TAC o CONV_RULE(REDEPTH_CONV RIGHT_IMP_FORALL_CONV)) THEN
  REWRITE_TAC[TAUT_CONV "a ==> b ==> c = a /\ b ==> c"] THEN
  DISCH_TAC THEN X_GEN_TAC "n:num" THEN
  REPEAT GEN_TAC THEN ASM_CASES_TAC "c = 1" THENL
   [ASM_REWRITE_TAC[EXP_1; MULT_EQ_1] THEN
    REPEAT STRIP_TAC THEN MAP_EVERY EXISTS_TAC ["1"; "1"] THEN
    ASM_REWRITE_TAC[MULT_CLAUSES; EXP_1];
    STRIP_TAC] THEN
  ASM_CASES_TAC "c = 0" THENL
   [UNDISCH_TAC "a * b = c EXP n" THEN
    STRUCT_CASES_TAC(SPEC "n:num" num_CASES) THEN
    ASM_REWRITE_TAC[MULT_EQ_0; EXP; MULT_CLAUSES; MULT_EQ_1] THEN
    STRIP_TAC THEN UNDISCH_TAC "coprime(a,b)" THEN
    ASM_REWRITE_TAC[ONCE_REWRITE_RULE[COPRIME_SYM] COPRIME_0; COPRIME_0] THEN
    DISCH_TAC THENL
     [MAP_EVERY EXISTS_TAC ["0"; "1"];
      MAP_EVERY EXISTS_TAC ["1"; "0"]] THEN
    ASM_REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES; EXP_1]; ALL_TAC] THEN
  FIRST_ASSUM(X_CHOOSE_THEN "p:num" MP_TAC o MATCH_MP PRIME_FACTOR) THEN
  STRIP_TAC THEN
  SUBGOAL_THEN "(p EXP n) divides a \/ (p EXP n) divides b" MP_TAC THENL
   [MATCH_MP_TAC PRIME_DIVPROD_POW THEN ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC DIVIDES_EXP THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
  UNDISCH_TAC "p divides c" THEN REWRITE_TAC[divides] THEN
  DISCH_THEN(X_CHOOSE_TAC "l:num") THEN
  SUBGOAL_THEN "~(p EXP n = 0)" ASSUME_TAC THENL
   [UNDISCH_TAC "c = p * l" THEN
    REWRITE_TAC[GSYM LESS_EQ_0; NOT_LESS_EQUAL] THEN
    STRUCT_CASES_TAC(SPEC "p:num" num_CASES) THEN
    ASM_REWRITE_TAC[MULT_CLAUSES; NOT_SUC; ZERO_LESS_EXP]; ALL_TAC] THEN
  DISCH_THEN(DISJ_CASES_THEN(X_CHOOSE_TAC "k:num")) THENL
   [SUBGOAL_THEN "?r s. (k = r EXP n) /\ (b = s EXP n)" STRIP_ASSUME_TAC THENL
     [FIRST_ASSUM MATCH_MP_TAC THEN EXISTS_TAC "l:num";
      MAP_EVERY EXISTS_TAC ["p * r"; "s:num"] THEN
      ASM_REWRITE_TAC[MULT_EXP]] THEN
    REPEAT CONJ_TAC THENL
     [MATCH_MP_TAC PRIME_FACTOR_LT THEN EXISTS_TAC "p:num" THEN
      ASM_REWRITE_TAC[];
      UNDISCH_TAC "coprime(a,b)" THEN ONCE_REWRITE_TAC[COPRIME_SYM] THEN
      ASM_REWRITE_TAC[COPRIME_LMUL2];
      MATCH_MP_TAC MULT_LCANCEL THEN EXISTS_TAC "p EXP n" THEN
      UNDISCH_TAC "a * b = c EXP n" THEN
      ASM_REWRITE_TAC[MULT_ASSOC; MULT_EXP]];
    SUBGOAL_THEN "?r s. (a = r EXP n) /\ (k = s EXP n)" STRIP_ASSUME_TAC THENL
     [FIRST_ASSUM MATCH_MP_TAC THEN EXISTS_TAC "l:num";
      MAP_EVERY EXISTS_TAC ["r:num"; "p * s"] THEN
      ASM_REWRITE_TAC[MULT_EXP]] THEN
    REPEAT CONJ_TAC THENL
     [MATCH_MP_TAC PRIME_FACTOR_LT THEN EXISTS_TAC "p:num" THEN
      ASM_REWRITE_TAC[];
      UNDISCH_TAC "coprime(a,b)" THEN ASM_REWRITE_TAC[COPRIME_LMUL2];
      ONCE_REWRITE_TAC[MULT_SYM] THEN
      MATCH_MP_TAC MULT_LCANCEL THEN EXISTS_TAC "p EXP n" THEN
      UNDISCH_TAC "a * b = c EXP n" THEN
      ASM_REWRITE_TAC[MULT_ASSOC; MULT_EXP] THEN
      DISCH_THEN(SUBST1_TAC o SYM) THEN
      CONV_TAC(AC_CONV(MULT_ASSOC,MULT_SYM))]]);;

%----------------------------------------------------------------------------%
% Classification of Pythagorean triples.                                     %
%----------------------------------------------------------------------------%

let PYTHAG_EVEN_LEMMA1 = prove_thm(`PYTHAG_EVEN_LEMMA1`,
  "!u v w. ((u EXP 2) + (v EXP 2) = w EXP 2) ==> ~(ODD(u) /\ ODD(v))",
  REPEAT GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] THEN
  DISCH_THEN(CONJUNCTS_THEN(CHOOSE_THEN SUBST1_TAC o MATCH_MP ODD_SQUARE)) THEN
  ONCE_REWRITE_TAC[(EQT_ELIM o AC_CONV(ADD_ASSOC,ADD_SYM))
   "(a + b) + (c + d) = (a + c) + (b + d)"] THEN
  DISJ_CASES_THEN MP_TAC (SPEC "w:num" EVEN_OR_ODD) THENL
   [DISCH_THEN(CHOOSE_THEN SUBST1_TAC o MATCH_MP EVEN_SQUARE);
    DISCH_THEN(CHOOSE_THEN SUBST1_TAC o MATCH_MP ODD_SQUARE)] THEN
  REWRITE_TAC[SYM(REDUCE_CONV "2 * 2")] THEN
  REWRITE_TAC[GSYM LEFT_ADD_DISTRIB; GSYM TIMES2; GSYM MULT_ASSOC] THEN
  REWRITE_TAC[CANCEL_TIMES2; GSYM ADD1; GSYM NOT_EVEN_EQ_ODD;
    NOT_EVEN_EQ_ODD]);;

let PYTHAG_EVEN_LEMMA2 = prove_thm(`PYTHAG_EVEN_LEMMA2`,
  "!u v. coprime(u,v) ==> ~(EVEN(u) /\ EVEN(v))",
  REPEAT GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN
  REWRITE_TAC[GSYM DIVIDES_2; divides] THEN
  STRIP_TAC THEN ASM_REWRITE_TAC[GCD_LMUL; COPRIME_GCD; MULT_EQ_1] THEN
  REDUCE_TAC THEN REWRITE_TAC[]);;

let PYTHAG_EVEN = prove_thm(`PYTHAG_EVEN`,
  "!u v w. ((u EXP 2) + (v EXP 2) = w EXP 2) /\ coprime(u,v)
        ==> (EVEN(u) /\ ODD(v) /\ ODD(w)) \/
            (ODD(u) /\ EVEN(v) /\ ODD(w))",
  REPEAT STRIP_TAC THEN
  FIRST_ASSUM(MP_TAC o MATCH_MP PYTHAG_EVEN_LEMMA1) THEN
  FIRST_ASSUM(MP_TAC o MATCH_MP PYTHAG_EVEN_LEMMA2) THEN
  REPEAT GEN_TAC THEN MAP_EVERY (DISJ_CASES_TAC o C SPEC EVEN_OR_ODD)
   ["u:num"; "v:num"; "w:num"] THEN ASM_REWRITE_TAC[] THEN
  ASM_REWRITE_TAC[GSYM EVEN_ODD; GSYM ODD_EVEN] THENL
   [DISJ1_TAC; DISJ2_TAC] THEN
  (SUBGOAL_THEN "~EVEN(w EXP 2)" MP_TAC THENL
    [FIRST_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[EVEN_ADD]; ALL_TAC] THEN
   ASM_REWRITE_TAC[num_CONV "2"; PARITY_EXP] THEN
   ASM_REWRITE_TAC[GSYM ODD_EVEN]));;

let PYTHAG_COCLASSIFY = prove_thm(`PYTHAG_COCLASSIFY`,
  "!u v w. ((u EXP 2) + (v EXP 2) = w EXP 2) /\ coprime(u,v) /\
           (EVEN(u) /\ ODD(v) /\ ODD(w)) ==>
                ?p q. coprime(p,q) /\
                      (u = 2 * p * q) /\
                      (v = (p EXP 2) - (q EXP 2)) /\
                      (w = (p EXP 2) + (q EXP 2))",
  REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP ADD_IMP_SUB) THEN
  REWRITE_TAC[DIFF_SQUARE] THEN RULE_ASSUM_TAC(REWRITE_RULE[ODD_EVEN]) THEN
  SUBGOAL_THEN "coprime(v,w)" ASSUME_TAC THENL
   [REWRITE_TAC[coprime] THEN X_GEN_TAC "d:num" THEN STRIP_TAC THEN
    SUBGOAL_THEN "d divides u" ASSUME_TAC THENL
     [MATCH_MP_TAC DIVIDES_REV THEN EXISTS_TAC "2" THEN
      REDUCE_TAC THEN REWRITE_TAC[] THEN
      MATCH_MP_TAC DIVIDES_ADD_REVR THEN EXISTS_TAC "v EXP 2" THEN
      ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[] THEN
      CONJ_TAC THEN MATCH_MP_TAC DIVIDES_EXP THEN ASM_REWRITE_TAC[];
      UNDISCH_TAC "coprime(u,v)" THEN REWRITE_TAC[coprime] THEN
      DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]; ALL_TAC] THEN
  ASM_CASES_TAC "u = 0" THENL
   [ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES] THEN
    DISCH_THEN(MP_TAC o REWRITE_RULE[MULT_EQ_0] o SYM) THEN
    REWRITE_TAC[ADD_EQ_0; SUB_EQ_0] THEN
    DISCH_THEN(DISJ_CASES_TAC) THENL
     [UNDISCH_TAC "coprime(u,v)" THEN ASM_REWRITE_TAC[COPRIME_0] THEN
      REDUCE_TAC THEN REWRITE_TAC[];
      UNDISCH_TAC "coprime(u,v)" THEN ONCE_REWRITE_TAC[COPRIME_SYM] THEN
      ASM_REWRITE_TAC[COPRIME_0] THEN DISCH_THEN SUBST_ALL_TAC THEN
      MAP_EVERY EXISTS_TAC ["1"; "0"] THEN
      REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; SUB_0] THEN
      UNDISCH_TAC "(u EXP 2) + (1 EXP 2) = w EXP 2" THEN
      ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES; ADD_CLAUSES] THEN
      DISCH_THEN(MP_TAC o SYM) THEN REWRITE_TAC[MULT_EQ_1] THEN
      DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[COPRIME_1]]; ALL_TAC] THEN
  SUBGOAL_THEN "EVEN(w + v)" (X_CHOOSE_TAC "r:num" o REWRITE_RULE[EVEN_EXISTS])
  THENL [ASM_REWRITE_TAC[EVEN_ADD]; ALL_TAC] THEN
  DISJ_CASES_TAC(SPECL ["v:num"; "w:num"] LESS_EQ_CASES) THENL
   [ALL_TAC;
    FIRST_ASSUM(\th. REWRITE_TAC[REWRITE_RULE[GSYM SUB_EQ_0] th]) THEN
    ASM_REWRITE_TAC[MULT_CLAUSES; EXP_2; MULT_EQ_0]] THEN
  SUBGOAL_THEN "EVEN(w - v)" (X_CHOOSE_TAC "s:num" o REWRITE_RULE[EVEN_EXISTS])
  THENL
   [UNDISCH_TAC "v <= w" THEN REWRITE_TAC[LESS_EQ_EXISTS] THEN
    DISCH_THEN(X_CHOOSE_THEN "d:num" SUBST_ALL_TAC) THEN
    UNDISCH_TAC "~EVEN(v + d)" THEN ASM_REWRITE_TAC[EVEN_ADD] THEN
    REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB]; ALL_TAC] THEN
  FIRST_ASSUM(X_CHOOSE_TAC "t:num" o REWRITE_RULE[EVEN_EXISTS]) THEN
  ASM_REWRITE_TAC[EXP_2] THEN ONCE_REWRITE_TAC[(EQT_ELIM o AC_CONV
    (MULT_ASSOC,MULT_SYM)) "(a * b) * (c * d) = (a * c) * (b * d)"] THEN
  REWRITE_TAC[REDUCE_CONV "2 * 2"; num_CONV "4"; MULT_MONO_EQ] THEN
  SUBGOAL_THEN "coprime(r,s)" ASSUME_TAC THENL
   [REWRITE_TAC[coprime] THEN X_GEN_TAC "d:num" THEN REWRITE_TAC[divides] THEN
    DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC "k:num") (X_CHOOSE_TAC "l:num"))
    THEN MAP_EVERY UNDISCH_TAC ["w + v = 2 * r"; "w - v = 2 * s"] THEN
    ASM_REWRITE_TAC[TAUT_CONV "a ==> b ==> c = a /\ b ==> c"] THEN
    DISCH_THEN(\th. let t2,t1 = CONJ_PAIR th in
     MP_TAC(MK_COMB(AP_TERM "$+" t1, t2)) THEN
     MP_TAC(MK_COMB(AP_TERM "$-" t1, t2))) THEN
    FIRST_ASSUM(\th. REWRITE_TAC[MATCH_MP ADD_SUM_DIFF th]) THEN
    REWRITE_TAC[GSYM LEFT_ADD_DISTRIB; GSYM LEFT_SUB_DISTRIB] THEN
    REWRITE_TAC[num_CONV "2"; MULT_MONO_EQ] THEN
    REPEAT DISCH_TAC THEN UNDISCH_TAC "coprime(v,w)" THEN
    ASM_REWRITE_TAC[coprime] THEN DISCH_THEN MATCH_MP_TAC THEN
    ASM_REWRITE_TAC[] THEN CONJ_TAC THEN
    MATCH_MP_TAC DIVIDES_RMUL THEN
    MATCH_ACCEPT_TAC DIVIDES_REFL;
    MP_TAC(ASSUME "coprime(r,s)") THEN
    REWRITE_TAC[TAUT_CONV "a ==> b ==> c = a /\ b ==> c"] THEN
    DISCH_THEN(MP_TAC o REWRITE_RULE[GSYM EXP_2] o GSYM) THEN
    DISCH_THEN(MP_TAC o MATCH_MP COPRIME_POW) THEN
    DISCH_THEN(X_CHOOSE_THEN "p:num" (X_CHOOSE_THEN "q:num"
      (CONJUNCTS_THEN SUBST_ALL_TAC))) THEN
    FIRST_ASSUM(MP_TAC o MATCH_MP ADD_SUM_DIFF) THEN
    ASM_REWRITE_TAC[GSYM LEFT_ADD_DISTRIB; GSYM LEFT_SUB_DISTRIB] THEN
    REWRITE_TAC[num_CONV "2"; MULT_MONO_EQ] THEN
    REWRITE_TAC[SYM(num_CONV "2")] THEN
    DISCH_THEN(CONJUNCTS_THEN(ASSUME_TAC o SYM)) THEN
    MAP_EVERY EXISTS_TAC ["p:num"; "q:num"] THEN
    ASM_REWRITE_TAC[GSYM DIFF_SQUARE; GSYM EXP_2] THEN
    UNDISCH_TAC "(u EXP 2) + (v EXP 2) = w EXP 2" THEN
    DISCH_THEN(MP_TAC o MATCH_MP ADD_IMP_SUB) THEN
    REWRITE_TAC[DIFF_SQUARE] THEN ASM_REWRITE_TAC[EXP_2] THEN
    ONCE_REWRITE_TAC[(EQT_ELIM o AC_CONV
     (MULT_ASSOC,MULT_SYM)) "(a * b) * (c * d) = (a * c) * (b * d)"] THEN
    REWRITE_TAC[REDUCE_CONV "2 * 2"; num_CONV "4"; MULT_MONO_EQ] THEN
    ONCE_REWRITE_TAC[(EQT_ELIM o AC_CONV
     (MULT_ASSOC,MULT_SYM)) "(a * b) * (c * d) = (a * c) * (b * d)"] THEN
    REWRITE_TAC[GSYM EXP_2] THEN REWRITE_TAC[num_CONV "2"] THEN
    REWRITE_TAC[EXP_MONO_EQ] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
    UNDISCH_TAC "coprime(p EXP 2,q EXP 2)" THEN
    REWRITE_TAC[num_CONV "2"; COPRIME_EXP2]]);;

%----------------------------------------------------------------------------%
% Now the main result                                                        %
%----------------------------------------------------------------------------%

let FLT42_DOWN_LEMMA1 = prove_thm(`FLT42_DOWN_LEMMA1`,
  "!x y z. ~coprime(x,y) /\
           ((x EXP 4) + (y EXP 4) = z EXP 2) /\
           ~(x = 0) /\ ~(y = 0)
        ==> ?u v w. ~(u = 0) /\ ~(v = 0) /\
                    ((u EXP 4) + (v EXP 4) = w EXP 2) /\ w < z",
  REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
  SUBGOAL_THEN "~(z EXP 2 = 0)" MP_TAC THENL
   [FIRST_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[EXP_EQ_0; ADD_EQ_0] THEN
    ASM_REWRITE_TAC[] THEN REDUCE_TAC;
    REWRITE_TAC[EXP_EQ_0] THEN REDUCE_TAC THEN DISCH_TAC] THEN
  REWRITE_TAC[COPRIME_PRIME_EQ] THEN
  CONV_TAC(ONCE_DEPTH_CONV NOT_FORALL_CONV) THEN REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN "p:num" STRIP_ASSUME_TAC) THEN
  SUBGOAL_THEN "(p EXP 2) divides z" MP_TAC THENL
   [MATCH_MP_TAC DIVIDES_REV THEN EXISTS_TAC "2" THEN REDUCE_TAC THEN
    REWRITE_TAC[GSYM EXP_4] THEN FIRST_ASSUM(SUBST1_TAC o SYM) THEN
    MATCH_MP_TAC DIVIDES_ADD THEN CONJ_TAC THEN
    MATCH_MP_TAC DIVIDES_EXP THEN ASM_REWRITE_TAC[];
    DISCH_THEN(X_CHOOSE_TAC "w:num" o REWRITE_RULE[divides])] THEN
  UNDISCH_TAC "p divides y" THEN REWRITE_TAC[divides] THEN
  DISCH_THEN(X_CHOOSE_TAC "v:num") THEN
  UNDISCH_TAC "p divides x" THEN REWRITE_TAC[divides] THEN
  DISCH_THEN(X_CHOOSE_TAC "u:num") THEN
  MAP_EVERY EXISTS_TAC ["u:num"; "v:num"; "w:num"] THEN
  UNDISCH_TAC "(x EXP 4) + (y EXP 4) = z EXP 2" THEN
  ASM_REWRITE_TAC[MULT_EXP; GSYM EXP_4; GSYM LEFT_ADD_DISTRIB] THEN
  SUBGOAL_THEN "~(p EXP 4 = 0)" MP_TAC THENL
   [REWRITE_TAC[EXP_EQ_0] THEN REDUCE_TAC THEN DISCH_THEN SUBST_ALL_TAC THEN
    UNDISCH_TAC "prime(0)" THEN REWRITE_TAC[PRIME_0];
    REWRITE_TAC[TAUT_CONV "a ==> b ==> c = a /\ b ==> c"]] THEN
  DISCH_THEN(\th. REWRITE_TAC[MATCH_MP MULT_LCANCEL th]) THEN
  UNDISCH_TAC "~(x = 0)" THEN ASM_REWRITE_TAC[MULT_EQ_0; DE_MORGAN_THM] THEN
  STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
  UNDISCH_TAC "~(y = 0)" THEN ASM_REWRITE_TAC[MULT_EQ_0; DE_MORGAN_THM] THEN
  STRIP_TAC THEN ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC LAND_CONV []
   [GSYM(el 3 (CONJUNCTS(SPEC_ALL MULT_CLAUSES)))] THEN
  ONCE_REWRITE_TAC[MULT_SYM] THEN
  UNDISCH_TAC "~(z = 0)" THEN ASM_REWRITE_TAC[] THEN
  STRUCT_CASES_TAC(SPEC "w:num" num_CASES) THENL
   [REWRITE_TAC[MULT_CLAUSES];
    DISCH_TAC THEN REWRITE_TAC[LESS_MULT_MONO]] THEN
  UNDISCH_TAC "prime(p)" THEN
  STRUCT_CASES_TAC(SPEC "p:num" num_CASES) THEN
  REWRITE_TAC[PRIME_0; EXP_2] THEN
  REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES; LESS_MONO_EQ; num_CONV "1"] THEN
  W(STRUCT_CASES_TAC o C SPEC num_CASES o hd o frees o snd) THEN
  REWRITE_TAC[SYM(num_CONV "1"); PRIME_1; ADD_CLAUSES; LESS_0]);;

let FLT42_DOWN_LEMMA2 = prove_thm(`FLT42_DOWN_LEMMA2`,
  "!x y z. ~(x = 0) /\ ~(y = 0) /\
           ((x EXP 4) + (y EXP 4) = z EXP 2) /\
           coprime(x EXP 2,y EXP 2) /\
           (EVEN(x EXP 2) /\ ODD(y EXP 2) /\ ODD(z))
        ==> ?u v w. ~(u = 0) /\ ~(v = 0) /\
                    ((u EXP 4) + (v EXP 4) = w EXP 2) /\ w < z",
  REPEAT GEN_TAC THEN REWRITE_TAC[EXP_4] THEN
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
  FIRST_ASSUM(MP_TAC o MATCH_MP PYTHAG_COCLASSIFY) THEN
  DISCH_THEN(X_CHOOSE_THEN "p:num" MP_TAC) THEN
  DISCH_THEN(X_CHOOSE_THEN "q:num" STRIP_ASSUME_TAC) THEN
  SUBGOAL_THEN "(q EXP 2) + (y EXP 2) = p EXP 2" ASSUME_TAC THENL
   [ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
    MATCH_MP_TAC SUB_ADD THEN ONCE_REWRITE_TAC[GSYM NOT_LESS] THEN
    DISCH_THEN(MP_TAC o MATCH_MP LESS_IMP_LESS_OR_EQ) THEN
    REWRITE_TAC[GSYM SUB_EQ_0] THEN DISCH_THEN SUBST_ALL_TAC THEN
    FIRST_ASSUM(UNDISCH_TAC o assert is_conj o concl) THEN
    ASM_REWRITE_TAC[ODD]; ALL_TAC] THEN
  SUBGOAL_THEN "coprime(q,y)" MP_TAC THENL
   [REWRITE_TAC[COPRIME_PRIME_EQ] THEN X_GEN_TAC "r:num" THEN
    STRIP_TAC THEN MP_TAC(ASSUME "coprime(p,q)") THEN
    REWRITE_TAC[COPRIME_PRIME_EQ] THEN
    DISCH_THEN(MP_TAC o SPEC "r:num") THEN ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC PRIME_DIVEXP THEN EXISTS_TAC "2" THEN
    ASM_REWRITE_TAC[] THEN
    FIRST_ASSUM(\th. GEN_REWRITE_TAC RAND_CONV [] [SYM th]) THEN
    MATCH_MP_TAC DIVIDES_ADD THEN REWRITE_TAC[num_CONV "2"] THEN CONJ_TAC THEN
    MATCH_MP_TAC DIVIDES_REXP THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
  DISCH_THEN(ASSUME_TAC o CONJ(ASSUME "(q EXP 2) + (y EXP 2) = p EXP 2")) THEN
  SUBGOAL_THEN "ODD(y)" ASSUME_TAC THENL
   [REWRITE_TAC[ODD_EVEN] THEN ONCE_REWRITE_TAC[GSYM(SPEC "1" PARITY_EXP)] THEN
    REWRITE_TAC[SYM(num_CONV "2"); GSYM ODD_EVEN] THEN
    FIRST_ASSUM(MATCH_ACCEPT_TAC o el 4 o CONJUNCTS); ALL_TAC] THEN
  FIRST_ASSUM(MP_TAC o MATCH_MP PYTHAG_EVEN) THEN
  ASM_REWRITE_TAC[EVEN_ODD] THEN REWRITE_TAC[GSYM EVEN_ODD] THEN STRIP_TAC THEN
  MP_TAC(SPECL ["q:num"; "y:num"; "p:num"] PYTHAG_COCLASSIFY) THEN
  ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN "a:num" MP_TAC) THEN
  DISCH_THEN(X_CHOOSE_THEN "b:num" STRIP_ASSUME_TAC) THEN
  MP_TAC(ASSUME "x EXP 2 = 2 * p * q") THEN
  REWRITE_TAC[ASSUME "p = (a EXP 2) + (b EXP 2)"; ASSUME "q = 2 * a * b"] THEN
  SUBGOAL_THEN "EVEN(x)" MP_TAC THENL
   [ONCE_REWRITE_TAC[GSYM(SPEC "1" PARITY_EXP)] THEN
    REWRITE_TAC[SYM(num_CONV "2"); GSYM ODD_EVEN] THEN
    FIRST_ASSUM(MATCH_ACCEPT_TAC o el 3 o CONJUNCTS); ALL_TAC] THEN
  REWRITE_TAC[EVEN_EXISTS] THEN
  DISCH_THEN(X_CHOOSE_THEN "x2:num" SUBST_ALL_TAC) THEN
  DISCH_THEN(MP_TAC o REWRITE_RULE[EXP_2; GSYM MULT_ASSOC]) THEN
  ONCE_REWRITE_TAC[(EQT_ELIM o AC_CONV(MULT_ASSOC,MULT_SYM))
    "m * n * p * q = (m * p) * n * q"] THEN REDUCE_TAC THEN
  REWRITE_TAC[GSYM MULT_ASSOC] THEN
  DISCH_THEN(MP_TAC o CONJ(EQF_ELIM(REDUCE_CONV "4 = 0"))) THEN
  DISCH_THEN(MP_TAC o MATCH_MP MULT_LCANCEL) THEN
  REWRITE_TAC[GSYM EXP_2] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN
  MP_TAC(MATCH_MP COPRIME_SOS (ASSUME "coprime(a,b)")) THEN
  ONCE_REWRITE_TAC[COPRIME_SYM] THEN DISCH_TAC THEN
  MP_TAC(SPECL ["2"; "(a EXP 2) + (b EXP 2)"; "a * b"; "x2:num"]
    COPRIME_POW) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN "Z:num" MP_TAC) THEN
  DISCH_THEN(X_CHOOSE_THEN "W:num" STRIP_ASSUME_TAC) THEN
  MP_TAC(SPECL ["2"; "a:num"; "b:num"; "W:num"] COPRIME_POW) THEN
  ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN "X:num" MP_TAC) THEN
  DISCH_THEN(X_CHOOSE_THEN "Y:num" (STRIP_ASSUME_TAC o GSYM)) THEN
  MAP_EVERY EXISTS_TAC ["X:num"; "Y:num"; "Z:num"] THEN ASM_REWRITE_TAC[] THEN
  SUBGOAL_THEN "~(W = 0)" ASSUME_TAC THENL
   [DISCH_TAC THEN UNDISCH_TAC "a * b = W EXP 2" THEN
    DISCH_THEN SUBST_ALL_TAC THEN
    UNDISCH_TAC "q = 2 * (W EXP 2)" THEN
    ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES] THEN
    DISCH_THEN SUBST_ALL_TAC THEN
    UNDISCH_TAC "(2 * x2) EXP 2 = 2 * p * 0" THEN
    REWRITE_TAC[MULT_CLAUSES; EXP_EQ_0] THEN
    REDUCE_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
  SUBGOAL_THEN "~(X EXP 2 = 0)" MP_TAC THENL
   [ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
    UNDISCH_TAC "a * b = W EXP 2" THEN
    ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES; MULT_EQ_0] THEN
    DISCH_THEN(MP_TAC o SYM) THEN ASM_REWRITE_TAC[MULT_EQ_0];
    REWRITE_TAC[EXP_EQ_0] THEN REDUCE_TAC THEN DISCH_TAC] THEN
  ASM_REWRITE_TAC[] THEN
  SUBGOAL_THEN "~(Y EXP 2 = 0)" MP_TAC THENL
   [ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
    UNDISCH_TAC "a * b = W EXP 2" THEN
    ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES; MULT_EQ_0] THEN
    DISCH_THEN(MP_TAC o SYM) THEN ASM_REWRITE_TAC[MULT_EQ_0];
    REWRITE_TAC[EXP_EQ_0] THEN REDUCE_TAC THEN DISCH_TAC] THEN
  ASM_REWRITE_TAC[] THEN
  SUBGOAL_THEN "~((2 * (W EXP 2)) EXP 2 = 0)" MP_TAC THENL
   [ASM_REWRITE_TAC[EXP_EQ_0; MULT_EQ_0] THEN REDUCE_TAC; ALL_TAC] THEN
  REWRITE_TAC[GSYM LESS_EQ_0; NOT_LESS_EQUAL] THEN DISCH_TAC THEN
  MATCH_MP_TAC LESS_EQ_LESS_TRANS THEN EXISTS_TAC "(Z EXP 2) EXP 2" THEN
  CONJ_TAC THENL
   [REWRITE_TAC[GSYM EXP_4] THEN
    STRUCT_CASES_TAC(SPEC "Z:num" num_CASES) THEN
    REWRITE_TAC[EXP_4; EXP_2; MULT_CLAUSES; LESS_EQ_REFL] THEN
    REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES; LESS_EQ_MONO] THEN
    REWRITE_TAC[GSYM ADD_ASSOC; LESS_EQ_ADD];
    GEN_REWRITE_TAC LAND_CONV [] [GSYM ADD_0] THEN
    ONCE_REWRITE_TAC[ADD_SYM] THEN
    ASM_REWRITE_TAC[LESS_MONO_ADD_EQ]]);;

let FLT42 = prove_thm(`FLT42`,
  "!z y x. ((x EXP 4) + (y EXP 4) = z EXP 2) ==> (x = 0) \/ (y = 0)",
  COMPLETE_INDUCT_TAC THEN X_GEN_TAC "z:num" THEN
  CONV_TAC CONTRAPOS_CONV THEN
  CONV_TAC(ONCE_DEPTH_CONV NOT_FORALL_CONV) THEN
  REWRITE_TAC[NOT_IMP] THEN
  CONV_TAC(TOP_DEPTH_CONV NOT_FORALL_CONV) THEN
  REWRITE_TAC[NOT_IMP; DE_MORGAN_THM] THEN
  DISCH_THEN(X_CHOOSE_THEN "y:num" MP_TAC) THEN
  DISCH_THEN(X_CHOOSE_THEN "x:num" STRIP_ASSUME_TAC) THEN
  ASM_CASES_TAC "coprime(x,y)" THENL
   [MP_TAC(SPECL ["x EXP 2"; "y EXP 2"; "z:num"] PYTHAG_EVEN) THEN
    ASM_REWRITE_TAC[GSYM EXP_4] THEN
    ASM_REWRITE_TAC[num_CONV "2"; COPRIME_EXP2] THEN
    REWRITE_TAC[SYM(num_CONV "2")] THEN
    DISCH_THEN DISJ_CASES_TAC THENL
     [MP_TAC(SPECL ["x:num"; "y:num"; "z:num"] FLT42_DOWN_LEMMA2) THEN
      ASM_REWRITE_TAC[] THEN
      ASM_REWRITE_TAC[num_CONV "2"; COPRIME_EXP2] THEN
      REWRITE_TAC[SYM(num_CONV "2")];
      MP_TAC(SPECL ["y:num"; "x:num"; "z:num"] FLT42_DOWN_LEMMA2) THEN
      ASM_REWRITE_TAC[] THEN
      ASM_REWRITE_TAC[num_CONV "2"; COPRIME_EXP2] THEN
      REWRITE_TAC[SYM(num_CONV "2")] THEN
      ONCE_REWRITE_TAC[COPRIME_SYM; ADD_SYM] THEN ASM_REWRITE_TAC[]];
  MP_TAC(SPECL ["x:num"; "y:num"; "z:num"] FLT42_DOWN_LEMMA1) THEN
  ASM_REWRITE_TAC[]] THEN
    DISCH_THEN(X_CHOOSE_THEN "u:num" MP_TAC) THEN
  DISCH_THEN(X_CHOOSE_THEN "v:num" MP_TAC) THEN
  DISCH_THEN(X_CHOOSE_THEN "w:num" STRIP_ASSUME_TAC) THEN
  EXISTS_TAC "w:num" THEN ASM_REWRITE_TAC[] THEN
  MAP_EVERY EXISTS_TAC ["v:num"; "u:num"] THEN ASM_REWRITE_TAC[]);;

%----------------------------------------------------------------------------%
% And now at last....                                                        %
%----------------------------------------------------------------------------%

let FLT4 = prove_thm(`FLT4`,
  "!x y z. ((x EXP 4) + (y EXP 4) = z EXP 4) ==> (x = 0) \/ (y = 0)",
  REPEAT GEN_TAC THEN SUBST1_TAC(SPEC "z:num" EXP_4) THEN
  MATCH_ACCEPT_TAC FLT42);;

close_theory();;