(* ========================================================================= *)
(* Analysis of solutions to Pell equation                                    *)
(* ========================================================================= *)

needs "Library/analysis.ml";;
needs "Library/transc.ml";;
needs "Library/prime.ml";;

prioritize_real();;

let PELL_INDUCTION = 
prove
 (`P 0 /\ P 1 /\ (!n. P n /\ P (n + 1) ==> P(n + 2)) ==> !n. P n`,

  STRIP_TAC THEN
  SUBGOAL_THEN `!n. P n /\ P(n + 1)` (fun th -> REWRITE_TAC[th]) THEN
  INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN
  ASM_SIMP_TAC[ADD1; ARITH_RULE `SUC(n + 1) = n + 2`]);;
(* ------------------------------------------------------------------------- *)
(* Useful number-theoretic basics                                            *)
(* ------------------------------------------------------------------------- *)

let ROOT_NONPOWER = 
prove
 (`!p q d n. ~(q = 0) /\ (p EXP n = d * q EXP n) ==> ?a. d = a EXP n`,

  REPEAT GEN_TAC THEN
  ASM_CASES_TAC `n = 0` THEN ASM_SIMP_TAC[EXP; MULT_CLAUSES] THEN
  STRIP_TAC THEN
  MP_TAC(SPECL [`n:num`; `q:num`; `p:num`] DIVIDES_EXP2_REV) THEN
  ASM_REWRITE_TAC[divides; LEFT_IMP_EXISTS_THM] THEN
  DISCH_THEN(MP_TAC o SPEC `d:num`) THEN
  REWRITE_TAC[EQT_INTRO(SPEC_ALL MULT_SYM)] THEN
  ONCE_REWRITE_TAC[MULT_SYM] THEN
  DISCH_THEN(X_CHOOSE_THEN `a:num` SUBST_ALL_TAC) THEN
  EXISTS_TAC `a:num` THEN
  UNDISCH_TAC `(a * q) EXP n = d * q EXP n` THEN
  ASM_SIMP_TAC[MULT_EXP; EQ_MULT_RCANCEL; EXP_EQ_0]);;
let INTEGER_SUB_LEMMA = 
prove
 (`!x y. ?n. (&x - &y) pow 2 = &n pow 2`,

  REPEAT STRIP_TAC THEN
  DISJ_CASES_THEN MP_TAC (SPECL [`&x`; `&y`] REAL_LE_TOTAL) THEN
  REWRITE_TAC[REAL_OF_NUM_LE] THEN DISCH_TAC THENL
   [EXISTS_TAC `y - x:num`; EXISTS_TAC `x - y:num`] THEN
  ASM_SIMP_TAC[GSYM REAL_OF_NUM_SUB] THEN
  REWRITE_TAC[REAL_POW_2] THEN REAL_ARITH_TAC);;
let SQRT_LINEAR_EQ = 
prove
 (`!a u v x y.
       2 <= a
       ==> ((&u + &v * sqrt(&a pow 2 - &1) = &x + &y * sqrt(&a pow 2 - &1)) <=>
            (u = x) /\ (v = y))`,

  REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN
  REWRITE_TAC[REAL_ARITH `(a + b = c + d) <=> (a - c = d - b)`] THEN
  REWRITE_TAC[GSYM REAL_SUB_RDISTRIB] THEN
  DISCH_THEN(MP_TAC o C AP_THM `2` o AP_TERM `(pow)`) THEN
  REWRITE_TAC[REAL_POW_MUL] THEN
  ASM_SIMP_TAC[SQRT_POW_2; REAL_SUB_LE; REAL_POW_LE_1; REAL_OF_NUM_LE;
               ARITH_RULE `2 <= a ==> 1 <= a`] THEN
  X_CHOOSE_TAC `p:num` (SPECL [`u:num`; `x:num`] INTEGER_SUB_LEMMA) THEN
  X_CHOOSE_TAC `q:num` (SPECL [`y:num`; `v:num`] INTEGER_SUB_LEMMA) THEN
  ASM_REWRITE_TAC[] THEN
  SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` SUBST1_TAC THENL
   [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
    ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
                 ARITH_RULE `2 <= a ==> 1 <= a`]; ALL_TAC] THEN
  REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_MUL; REAL_OF_NUM_EQ] THEN
  DISCH_TAC THEN
  MP_TAC(SPECL [`p:num`; `q:num`; `a EXP 2 - 1`; `2`] ROOT_NONPOWER) THEN
  ASM_REWRITE_TAC[EQT_INTRO(SPEC_ALL MULT_SYM)] THEN
  MATCH_MP_TAC(TAUT `~b /\ (a ==> c) ==> ((~a ==> b) ==> c)`) THEN
  CONJ_TAC THENL
   [DISCH_THEN(X_CHOOSE_THEN `b:num` MP_TAC) THEN
    DISCH_THEN(MP_TAC o MATCH_MP
     (ARITH_RULE `(a - 1 = b) ==> 1 < a ==> (a - b = 1)`)) THEN
    SUBST1_TAC(SYM(SPEC `a:num` (CONJUNCT1 EXP))) THEN
    ASM_REWRITE_TAC[LT_EXP; ARITH_LE; ARITH_LT] THEN
    REWRITE_TAC[EXP] THEN
    DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
      `(a - b = 1) ==> (a = b + 1)`)) THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_ADD; GSYM
                REAL_OF_NUM_POW] THEN
    REWRITE_TAC[REAL_POW_2] THEN
    DISCH_THEN(MP_TAC o MATCH_MP
     (REAL_ARITH `(a * a = b * b + &1) ==> ((a + b) * (a - b) = &1)`)) THEN
    DISCH_THEN(MP_TAC o C AP_THM `2` o AP_TERM `(pow)`) THEN
    REWRITE_TAC[REAL_POW_MUL] THEN
    X_CHOOSE_TAC `c:num` (SPECL [`a:num`; `b:num`] INTEGER_SUB_LEMMA) THEN
    ASM_REWRITE_TAC[] THEN
    REWRITE_TAC[GSYM REAL_POW_MUL] THEN
    REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_MUL; REAL_OF_NUM_ADD] THEN
    REWRITE_TAC[REAL_OF_NUM_EQ; EXP_ONE; EXP_EQ_1; MULT_EQ_1; ARITH_EQ] THEN
    UNDISCH_TAC `2 <= a` THEN ARITH_TAC;
    DISCH_THEN SUBST_ALL_TAC THEN
    UNDISCH_TAC `p EXP 2 = 0 EXP 2 * (a EXP 2 - 1)` THEN
    REWRITE_TAC[ARITH; MULT_CLAUSES; EXP_EQ_0] THEN
    DISCH_THEN SUBST_ALL_TAC THEN
    UNDISCH_TAC `(&u - &x) pow 2 = &0 pow 2` THEN
    UNDISCH_TAC `(&y - &v) pow 2 = &0 pow 2` THEN
    CONV_TAC REAL_RAT_REDUCE_CONV THEN
    REWRITE_TAC[REAL_POW_EQ_0; ARITH_EQ; REAL_SUB_0] THEN
    SIMP_TAC[REAL_OF_NUM_EQ]]);;
(* ------------------------------------------------------------------------- *)
(* Recurrence defining the solutions.                                        *)
(* ------------------------------------------------------------------------- *)

let X_DEF =
  
let th = 
prove
   (`!a. ?X. !n. X n = if n = 0 then 1
                       else if n = 1 then a
                       else 2 * a * X(n-1) - X(n-2)`,

    GEN_TAC THEN MATCH_MP_TAC(MATCH_MP WF_REC WF_num) THEN
    REPEAT STRIP_TAC THEN
    REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
    BINOP_TAC THEN
    ASM_SIMP_TAC[ARITH_RULE `n - m < n <=> ~(m = 0) /\ ~(n = 0)`; ARITH_EQ]) in
  new_specification ["X"] (REWRITE_RULE[SKOLEM_THM] th);;
let X_CLAUSES = 
prove
 (`(!a. X a 0 = 1) /\
   (!a. X a 1 = a) /\
   (!a n. X a (n + 2) = 2 * a * X a (n + 1) - X a (n))`,

  REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [X_DEF] THEN
  REWRITE_TAC[ARITH_EQ; ADD_EQ_0; ARITH_RULE `~(n + 2 = 1)`] THEN
  REWRITE_TAC[ARITH_RULE `((n + 2) - 2 = n) /\ ((n + 2) - 1 = n + 1)`]);;
let Y_DEF =
  
let th = 
prove
   (`!a. ?Y. !n. Y n = if n = 0 then 0
                       else if n = 1 then 1
                       else 2 * a * Y(n-1) - Y(n-2)`,

    GEN_TAC THEN MATCH_MP_TAC(MATCH_MP WF_REC WF_num) THEN
    REPEAT STRIP_TAC THEN
    REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
    BINOP_TAC THEN
    ASM_SIMP_TAC[ARITH_RULE `n - m < n <=> ~(m = 0) /\ ~(n = 0)`; ARITH_EQ]) in
  new_specification ["Y"] (REWRITE_RULE[SKOLEM_THM] th);;
let Y_CLAUSES = 
prove
 (`(!a. Y a 0 = 0) /\
   (!a. Y a 1 = 1) /\
   (!a n. Y a (n + 2) = 2 * a * Y a (n + 1) - Y a (n))`,

  REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [Y_DEF] THEN
  REWRITE_TAC[ARITH_EQ; ADD_EQ_0; ARITH_RULE `~(n + 2 = 1)`] THEN
  REWRITE_TAC[ARITH_RULE `((n + 2) - 2 = n) /\ ((n + 2) - 1 = n + 1)`]);;
(* ------------------------------------------------------------------------- *)
(* An obvious but tiresome lemma: the Xs and Ys increase.                    *)
(* ------------------------------------------------------------------------- *)

let X_INCREASES = 
prove
 (`!a n. ~(a = 0) ==> X a n <= X a (n + 1)`,

  GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
  MATCH_MP_TAC num_WF THEN REPEAT STRIP_TAC THEN
  ASM_CASES_TAC `n = 0` THEN
  ASM_REWRITE_TAC[X_CLAUSES; ADD_CLAUSES;
    ARITH_RULE `1 <= a <=> ~(a = 0)`] THEN
  GEN_REWRITE_TAC RAND_CONV [X_DEF] THEN
  ASM_REWRITE_TAC[ADD_EQ_0; ARITH_EQ;
    ARITH_RULE `(n + 1 = 1) <=> (n = 0)`] THEN
  REWRITE_TAC[ADD_SUB] THEN
  MATCH_MP_TAC(ARITH_RULE `a + b <= c ==> a <= c - b:num`) THEN
  MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `2 * X a n` THEN CONJ_TAC THENL
   [ALL_TAC;
    REWRITE_TAC[LE_MULT_LCANCEL; ARITH_EQ] THEN
    UNDISCH_TAC `~(a = 0)` THEN SPEC_TAC(`a:num`,`a:num`) THEN
    INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
    REWRITE_TAC[ARITH_RULE `a <= b + a:num`]] THEN
  MATCH_MP_TAC(ARITH_RULE `b <= a ==> a + b <= 2 * a`) THEN
  SUBGOAL_THEN `n = (n - 1) + 1` SUBST1_TAC THENL
   [UNDISCH_TAC `~(n = 0)` THEN ARITH_TAC; ALL_TAC] THEN
  REWRITE_TAC[ARITH_RULE `((n + 1) + 1) - 2 = n`] THEN
  FIRST_ASSUM MATCH_MP_TAC THEN
  UNDISCH_TAC `~(n = 0)` THEN ARITH_TAC);;
let Y_INCREASES = 
prove
 (`!a n. ~(a = 0) ==> Y a n <= Y a (n + 1)`,

  GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
  MATCH_MP_TAC num_WF THEN REPEAT STRIP_TAC THEN
  ASM_CASES_TAC `n = 0` THEN
  ASM_REWRITE_TAC[Y_CLAUSES; ADD_CLAUSES; LE_0] THEN
  GEN_REWRITE_TAC RAND_CONV [Y_DEF] THEN
  ASM_REWRITE_TAC[ADD_EQ_0; ARITH_EQ;
    ARITH_RULE `(n + 1 = 1) <=> (n = 0)`] THEN
  REWRITE_TAC[ADD_SUB] THEN
  MATCH_MP_TAC(ARITH_RULE `a + b <= c ==> a <= c - b:num`) THEN
  MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `2 * Y a n` THEN CONJ_TAC THENL
   [ALL_TAC;
    REWRITE_TAC[LE_MULT_LCANCEL; ARITH_EQ] THEN
    UNDISCH_TAC `~(a = 0)` THEN SPEC_TAC(`a:num`,`a:num`) THEN
    INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
    REWRITE_TAC[ARITH_RULE `a <= b + a:num`]] THEN
  MATCH_MP_TAC(ARITH_RULE `b <= a ==> a + b <= 2 * a`) THEN
  SUBGOAL_THEN `n = (n - 1) + 1` SUBST1_TAC THENL
   [UNDISCH_TAC `~(n = 0)` THEN ARITH_TAC; ALL_TAC] THEN
  REWRITE_TAC[ARITH_RULE `((n + 1) + 1) - 2 = n`] THEN
  FIRST_ASSUM MATCH_MP_TAC THEN
  UNDISCH_TAC `~(n = 0)` THEN ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Show that the expression is a power of the basis.                         *)
(* ------------------------------------------------------------------------- *)

let XY_POWER_POS = 
prove
 (`!a n. ~(a = 0) ==> (&(X a n) + &(Y a n) * sqrt(&a pow 2 - &1) =
                       (&a + sqrt(&a pow 2 - &1)) pow n)`,

  GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
  MATCH_MP_TAC num_WF THEN GEN_TAC THEN DISCH_TAC THEN
  ONCE_REWRITE_TAC[X_DEF; Y_DEF] THEN
  COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH_EQ] THEN
  REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID; real_pow] THEN
  COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_POW_1; REAL_MUL_LID] THEN
  REWRITE_TAC[REAL_OF_NUM_ADD] THEN
  SUBGOAL_THEN
   `(&(2 * a * X a (n - 1) - X a (n - 2)) =
     &(2 * a * X a (n - 1)) - &(X a (n - 2))) /\
    (&(2 * a * Y a (n - 1) - Y a (n - 2)) =
     &(2 * a * Y a (n - 1)) - &(Y a (n - 2)))`
   (CONJUNCTS_THEN SUBST1_TAC)
  THENL
   [CONJ_TAC THEN MATCH_MP_TAC(GSYM REAL_OF_NUM_SUB) THEN
    MATCH_MP_TAC(ARITH_RULE
     `x <= y /\ y <= 2 * a * y ==> x <= 2 * a * y`) THEN
    ASM_SIMP_TAC[ARITH_RULE
     `~(n = 0) /\ ~(n = 1) ==> (n - 1 = (n - 2) + 1)`] THEN
    ASM_SIMP_TAC[X_INCREASES; Y_INCREASES] THEN
    REWRITE_TAC[MULT_ASSOC] THEN
    GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `n = 1 * n`] THEN
    REWRITE_TAC[LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
    UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC; ALL_TAC] THEN
  REWRITE_TAC[REAL_ARITH
   `(x1 - x2) + (y1 - y2) * a = (x1 + y1 * a) - (x2 + y2 * a)`] THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
  REWRITE_TAC[GSYM REAL_MUL_ASSOC; GSYM REAL_ADD_LDISTRIB] THEN
  ASM_SIMP_TAC[ARITH_RULE
   `~(n = 0) /\ ~(n = 1) ==> n - 2 < n /\ n - 1 < n`] THEN
  ASM_SIMP_TAC[ARITH_RULE
     `~(n = 0) /\ ~(n = 1) ==> (n - 1 = 1 + (n - 2))`] THEN
  REWRITE_TAC[REAL_POW_ADD; REAL_MUL_ASSOC; REAL_POW_1] THEN
  REWRITE_TAC[REAL_ARITH `a * b - b = (a - &1) * b`] THEN
  SUBGOAL_THEN `n = 2 + (n - 2)`
    (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th])
  THENL
   [MAP_EVERY UNDISCH_TAC [`~(n = 0)`; `~(n = 1)`] THEN ARITH_TAC;
    ALL_TAC] THEN
  REWRITE_TAC[REAL_POW_ADD] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
  REWRITE_TAC[REAL_POW_2; REAL_ADD_LDISTRIB; REAL_ADD_RDISTRIB] THEN
  REWRITE_TAC[GSYM REAL_POW_2] THEN
  ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2; REAL_SUB_LE;
               REAL_POW_LE_1; REAL_OF_NUM_LE;
               ARITH_RULE `1 <= a <=> ~(a = 0)`] THEN
  REWRITE_TAC[REAL_POW_2] THEN REAL_ARITH_TAC);;
let XY_POWER_NEG = 
prove
 (`!a n. ~(a = 0) ==> (&(X a n) - &(Y a n) * sqrt(&a pow 2 - &1) =
                       (&a - sqrt(&a pow 2 - &1)) pow n)`,

  GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
  MATCH_MP_TAC num_WF THEN GEN_TAC THEN DISCH_TAC THEN
  ONCE_REWRITE_TAC[X_DEF; Y_DEF] THEN
  COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH_EQ] THEN
  REWRITE_TAC[REAL_MUL_LZERO; REAL_SUB_RZERO; real_pow] THEN
  COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_POW_1; REAL_MUL_LID] THEN
  REWRITE_TAC[REAL_OF_NUM_ADD] THEN
  SUBGOAL_THEN
   `(&(2 * a * X a (n - 1) - X a (n - 2)) =
     &(2 * a * X a (n - 1)) - &(X a (n - 2))) /\
    (&(2 * a * Y a (n - 1) - Y a (n - 2)) =
     &(2 * a * Y a (n - 1)) - &(Y a (n - 2)))`
   (CONJUNCTS_THEN SUBST1_TAC)
  THENL
   [CONJ_TAC THEN MATCH_MP_TAC(GSYM REAL_OF_NUM_SUB) THEN
    MATCH_MP_TAC(ARITH_RULE
     `x <= y /\ y <= 2 * a * y ==> x <= 2 * a * y`) THEN
    ASM_SIMP_TAC[ARITH_RULE
     `~(n = 0) /\ ~(n = 1) ==> (n - 1 = (n - 2) + 1)`] THEN
    ASM_SIMP_TAC[X_INCREASES; Y_INCREASES] THEN
    REWRITE_TAC[MULT_ASSOC] THEN
    GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `n = 1 * n`] THEN
    REWRITE_TAC[LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
    UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC; ALL_TAC] THEN
  REWRITE_TAC[REAL_ARITH
   `(x1 - x2) - (y1 - y2) * a = (x1 - y1 * a) - (x2 - y2 * a)`] THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
  REWRITE_TAC[GSYM REAL_MUL_ASSOC; GSYM REAL_SUB_LDISTRIB] THEN
  ASM_SIMP_TAC[ARITH_RULE
   `~(n = 0) /\ ~(n = 1) ==> n - 2 < n /\ n - 1 < n`] THEN
  ASM_SIMP_TAC[ARITH_RULE
     `~(n = 0) /\ ~(n = 1) ==> (n - 1 = 1 + (n - 2))`] THEN
  REWRITE_TAC[REAL_POW_ADD; REAL_MUL_ASSOC; REAL_POW_1] THEN
  REWRITE_TAC[REAL_ARITH `a * b - b = (a - &1) * b`] THEN
  SUBGOAL_THEN `n = 2 + (n - 2)`
    (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th])
  THENL
   [MAP_EVERY UNDISCH_TAC [`~(n = 0)`; `~(n = 1)`] THEN ARITH_TAC;
    ALL_TAC] THEN
  REWRITE_TAC[REAL_POW_ADD] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
  REWRITE_TAC[REAL_POW_2; REAL_SUB_LDISTRIB; REAL_SUB_RDISTRIB] THEN
  REWRITE_TAC[GSYM REAL_POW_2] THEN
  ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2; REAL_SUB_LE;
               REAL_POW_LE_1; REAL_OF_NUM_LE;
               ARITH_RULE `1 <= a <=> ~(a = 0)`] THEN
  REWRITE_TAC[REAL_POW_2] THEN REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Hence all members of recurrence relations are Pell solutions.             *)
(* ------------------------------------------------------------------------- *)

let XY_ARE_SOLUTIONS = 
prove
 (`!a n. ~(a = 0)
         ==> ((X a n) EXP 2 = (a EXP 2 - 1) * (Y a n) EXP 2 + 1)`,

  REPEAT STRIP_TAC THEN
  FIRST_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP XY_POWER_NEG) THEN
  FIRST_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP XY_POWER_POS) THEN
  REWRITE_TAC[IMP_IMP] THEN
  DISCH_THEN(fun th ->
   MP_TAC(MK_COMB(AP_TERM `( * )` (CONJUNCT1 th),CONJUNCT2 th))) THEN
  REWRITE_TAC[GSYM REAL_POW_MUL] THEN
  REWRITE_TAC[REAL_ARITH `(x + y) * (x - y) = x * x - y * y`] THEN
  ONCE_REWRITE_TAC[AC REAL_MUL_AC
    `(a * b) * (c * d) = (a * c) * (b * d)`] THEN
  ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2; REAL_SUB_LE;
               REAL_POW_LE_1; REAL_OF_NUM_LE;
               ARITH_RULE `1 <= a <=> ~(a = 0)`] THEN
  REWRITE_TAC[REAL_ARITH `a - (a - &1) = &1`; REAL_POW_ONE] THEN
  REWRITE_TAC[REAL_EQ_SUB_RADD] THEN
  SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` SUBST1_TAC THENL
   [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
    ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
                 ARITH_RULE `1 <= a <=> ~(a = 0)`];
    REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_MUL; REAL_OF_NUM_EQ;
                REAL_OF_NUM_POW] THEN
    REWRITE_TAC[MULT_AC; ADD_AC]]);;
(* ------------------------------------------------------------------------- *)
(* And they are all solutions.                                               *)
(* ------------------------------------------------------------------------- *)

let X_DEGENERATE = 
prove
 (`!n. X 1 n = 1`,

  MATCH_MP_TAC PELL_INDUCTION THEN SIMP_TAC[X_CLAUSES; ARITH]);;
let Y_DEGENERATE = 
prove
 (`!n. Y 1 n = n`,

  MATCH_MP_TAC PELL_INDUCTION THEN SIMP_TAC[Y_CLAUSES] THEN
  REPEAT STRIP_TAC THEN ARITH_TAC);;
let REAL_ARCH_POW = 
prove
 (`!x y. &1 < x /\ &1 < y
         ==> ?n. x pow n <= y /\ y < x pow (SUC n)`,

  REPEAT STRIP_TAC THEN
  MP_TAC(SPEC `ln(x)` REAL_ARCH_LEAST) THEN ASM_SIMP_TAC[LN_POS_LT] THEN
  DISCH_THEN(MP_TAC o SPEC `ln(y)`) THEN
  ASM_SIMP_TAC[LN_POS_LT; REAL_LT_IMP_LE] THEN
  ASM_SIMP_TAC[GSYM LN_POW; REAL_ARITH `&1 < x ==> &0 < x`;
               REAL_POW_LT; LN_MONO_LT; LN_MONO_LE]);;
let SOLUTIONS_INDUCTION = 
prove
 (`!a x y.
        ~(a = 0) /\ ~(a = 1) /\ ~(y = 0) /\
        (x EXP 2 = (a EXP 2 - 1) * y EXP 2 + 1)
        ==> ?x' y'. x' < x /\ y' < y /\
                    (x' EXP 2 = (a EXP 2 - 1) * y' EXP 2 + 1) /\
                    (&x + &y * sqrt(&a pow 2 - &1) =
                     (&x' + &y' * sqrt(&a pow 2 - &1)) *
                     (&a + sqrt(&a pow 2 - &1)))`,

  REPEAT STRIP_TAC THEN
  EXISTS_TAC `a * x - (a EXP 2 - 1) * y` THEN
  EXISTS_TAC `a * y - x:num` THEN
  SUBGOAL_THEN `x <= a * y:num` ASSUME_TAC THENL
   [ONCE_REWRITE_TAC[GSYM(SPECL [`x:num`; `y:num`; `1`] EXP_MONO_LE_SUC)] THEN
    ASM_REWRITE_TAC[ARITH_SUC] THEN
    REWRITE_TAC[GSYM ADD1; LE_SUC_LT] THEN
    REWRITE_TAC[MULT_EXP; LT_MULT_RCANCEL] THEN
    REWRITE_TAC[ARITH_RULE `a - 1 < a <=> ~(a = 0)`] THEN
    ASM_REWRITE_TAC[EXP_EQ_0]; ALL_TAC] THEN
  SUBGOAL_THEN `(a EXP 2 - 1) * y <= a * x:num` ASSUME_TAC THENL
   [SUBGOAL_THEN `(a EXP 2 - 1) * y EXP 2 < a * x * y` MP_TAC THENL
     [ALL_TAC;
      ASM_SIMP_TAC[MULT_ASSOC; EXP_2; LT_MULT_RCANCEL; LT_IMP_LE]] THEN
    REWRITE_TAC[GSYM LE_SUC_LT; ADD1] THEN
    FIRST_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [SYM th]) THEN
    GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
    REWRITE_TAC[EXP_2; GSYM MULT_ASSOC; LE_MULT_LCANCEL] THEN
    DISJ2_TAC THEN ONCE_REWRITE_TAC[MULT_SYM] THEN ASM_REWRITE_TAC[];
    ALL_TAC] THEN
  MATCH_MP_TAC(TAUT `d /\ (d ==> a /\ b /\ c)
                     ==> a /\ b /\ c /\ d`) THEN
  CONJ_TAC THENL
   [MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN
    EXISTS_TAC `&a - sqrt(&a pow 2 - &1)` THEN CONJ_TAC THENL
     [REWRITE_TAC[REAL_SUB_0] THEN
      DISCH_THEN(MP_TAC o C AP_THM `2` o AP_TERM `(pow)`) THEN
      ASM_SIMP_TAC[SQRT_POW_2; REAL_SUB_LE; REAL_POW_LE_1; REAL_OF_NUM_LE;
                   ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
      REAL_ARITH_TAC; ALL_TAC] THEN
    REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
    REWRITE_TAC[REAL_ARITH `(a + b) * (a - b) = a * a - b * b`] THEN
    ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2;  REAL_SUB_LE; REAL_POW_LE_1;
                 REAL_OF_NUM_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
    REWRITE_TAC[REAL_ARITH `a - (a - b) = b`; REAL_MUL_RID] THEN
    ASM_SIMP_TAC[GSYM REAL_OF_NUM_SUB] THEN
    REWRITE_TAC[REAL_ARITH
     `(x + y * s) * (a - s) = (a * x - (s * s) * y) + (a * y - x) * s`] THEN
    ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2;  REAL_SUB_LE; REAL_POW_LE_1;
                 REAL_OF_NUM_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
    AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
    AP_THM_TAC THEN AP_TERM_TAC THEN
    REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
    ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
                 ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
  DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
  SUBGOAL_THEN
   `(&x - &y * sqrt(&a pow 2 - &1)) =
    (&(a * x - (a EXP 2 - 1) * y) - &(a * y - x) * sqrt (&a pow 2 - &1)) *
    (&a - sqrt(&a pow 2 - &1))`
  MP_TAC THENL
   [MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN
    EXISTS_TAC `&a + sqrt(&a pow 2 - &1)` THEN CONJ_TAC THENL
     [MATCH_MP_TAC(REAL_ARITH `~(a = --b) ==> ~(a + b = &0)`) THEN
      DISCH_THEN(MP_TAC o C AP_THM `2` o AP_TERM `(pow)`) THEN
      REWRITE_TAC[REAL_POW_NEG; ARITH] THEN
      ASM_SIMP_TAC[SQRT_POW_2; REAL_SUB_LE; REAL_POW_LE_1; REAL_OF_NUM_LE;
                   ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
      REAL_ARITH_TAC; ALL_TAC] THEN
    REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
    REWRITE_TAC[REAL_ARITH `(a - b) * (a + b) = a * a - b * b`] THEN
    ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2;  REAL_SUB_LE; REAL_POW_LE_1;
                 REAL_OF_NUM_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
    REWRITE_TAC[REAL_ARITH `a - (a - b) = b`; REAL_MUL_RID] THEN
    ASM_SIMP_TAC[GSYM REAL_OF_NUM_SUB] THEN
    REWRITE_TAC[REAL_ARITH
     `(x - y * s) * (a + s) = (a * x - (s * s) * y) - (a * y - x) * s`] THEN
    ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2;  REAL_SUB_LE; REAL_POW_LE_1;
                 REAL_OF_NUM_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
    AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
    AP_THM_TAC THEN AP_TERM_TAC THEN
    REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
    ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
                 ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
  DISCH_THEN(fun th1 -> DISCH_THEN (fun th2 ->
   MP_TAC(MK_COMB(AP_TERM `( * )` th1,th2)))) THEN
  ONCE_REWRITE_TAC[AC REAL_MUL_AC
   `(a * b) * (c * d) = (c * a) * (d * b)`] THEN
  REWRITE_TAC[REAL_ARITH `(a + b) * (a - b) = a * a - b * b`] THEN
  REWRITE_TAC[REAL_ARITH `(a - b) * (a + b) = a * a - b * b`] THEN
  ONCE_REWRITE_TAC[AC REAL_MUL_AC
   `(a * b) * (c * b) = (c * a) * (b * b)`] THEN
  ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2;  REAL_SUB_LE; REAL_POW_LE_1;
               REAL_OF_NUM_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
  REWRITE_TAC[REAL_ARITH `a - (a - b) = b`; REAL_MUL_RID] THEN
  ASM_REWRITE_TAC[REAL_OF_NUM_POW] THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_POW; GSYM REAL_OF_NUM_ADD;
              GSYM REAL_OF_NUM_MUL] THEN
  SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` (SUBST1_TAC o SYM) THENL
   [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
    ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
                 ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
  DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
   `((a * b + &1) - b * a = x - y) ==> (x = y + &1)`)) THEN
  SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` SUBST1_TAC THENL
   [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
    ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
                 ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
  ASM_SIMP_TAC[REAL_OF_NUM_SUB; REAL_OF_NUM_ADD; REAL_OF_NUM_EQ;
               REAL_OF_NUM_POW; REAL_OF_NUM_MUL] THEN
  ABBREV_TAC `u = a * x - (a EXP 2 - 1) * y` THEN
  ABBREV_TAC `v = a * y - x:num` THEN
  DISCH_THEN(ASSUME_TAC o ONCE_REWRITE_RULE[MULT_SYM]) THEN
  REWRITE_TAC[MULT_AC] THEN
  MATCH_MP_TAC(TAUT `(a <=> b) /\ (~a /\ ~b ==> F) ==> a /\ b`) THEN
  CONJ_TAC THENL
   [GEN_REWRITE_TAC LAND_CONV [GSYM(SPEC `1` EXP_MONO_LT_SUC)] THEN
    ASM_REWRITE_TAC[ARITH_SUC] THEN
    REWRITE_TAC[LT_ADD_RCANCEL; LT_MULT_LCANCEL] THEN
    REWRITE_TAC[num_CONV `2`; EXP_MONO_LT_SUC] THEN
    MATCH_MP_TAC(TAUT `a ==> (a /\ b <=> b)`) THEN
    REWRITE_TAC[SUB_EQ_0; ARITH_SUC; NOT_LE] THEN
    SUBST1_TAC(SYM(SPEC `a:num` (CONJUNCT1 EXP))) THEN
    REWRITE_TAC[LT_EXP] THEN REWRITE_TAC[ARITH] THEN
    MATCH_MP_TAC(ARITH_RULE `~(a = 0) /\ ~(a = 1) ==> 2 <= a`) THEN
    ASM_REWRITE_TAC[]; ALL_TAC] THEN
  REWRITE_TAC[NOT_LT] THEN STRIP_TAC THEN
  UNDISCH_TAC
   `&x + &y * sqrt (&a pow 2 - &1) =
    (&u + &v * sqrt (&a pow 2 - &1)) * (&a + sqrt (&a pow 2 - &1))` THEN
  REWRITE_TAC[] THEN
  MATCH_MP_TAC(REAL_ARITH `a < b ==> ~(a = b)`) THEN
  MATCH_MP_TAC REAL_LET_TRANS THEN
  EXISTS_TAC `(&u + &v * sqrt (&a pow 2 - &1)) * &1` THEN CONJ_TAC THENL
   [REWRITE_TAC[REAL_MUL_RID] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN
    ASM_REWRITE_TAC[REAL_OF_NUM_LE] THEN
    MATCH_MP_TAC REAL_LE_RMUL THEN
    ASM_SIMP_TAC[REAL_OF_NUM_LE; SQRT_POS_LE; REAL_POW_LE_1;
                 REAL_SUB_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`];
    ALL_TAC] THEN
  MATCH_MP_TAC REAL_LT_LMUL THEN CONJ_TAC THENL
   [MATCH_MP_TAC REAL_LTE_ADD THEN CONJ_TAC THENL
     [REWRITE_TAC[REAL_OF_NUM_LT; LT_NZ] THEN DISCH_THEN SUBST_ALL_TAC THEN
      UNDISCH_TAC `0 EXP 2 = (a EXP 2 - 1) * v EXP 2 + 1` THEN
      DISCH_THEN(MP_TAC o SYM) THEN CONV_TAC NUM_REDUCE_CONV THEN
      REWRITE_TAC[ADD_EQ_0; ARITH_EQ]; ALL_TAC] THEN
    MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_POS] THEN
    ASM_SIMP_TAC[REAL_OF_NUM_LE; SQRT_POS_LE; REAL_POW_LE_1;
                 REAL_SUB_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`];
    ALL_TAC] THEN
  MATCH_MP_TAC(REAL_ARITH `&1 < x /\ &0 <= y ==> &1 < x + y`) THEN
  ASM_SIMP_TAC[REAL_OF_NUM_LE; SQRT_POS_LE; REAL_POW_LE_1;
               REAL_SUB_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
  REWRITE_TAC[REAL_OF_NUM_LT] THEN
  MATCH_MP_TAC(ARITH_RULE `~(a = 0) /\ ~(a = 1) ==> 1 < a`) THEN
  ASM_REWRITE_TAC[]);;
let SOLUTIONS_ARE_XY = 
prove
 (`!a x y.
    ~(a = 0) /\
    (x EXP 2 = (a EXP 2 - 1) * y EXP 2 + 1)
    ==> ?n. (x = X a n) /\ (y = Y a n)`,

  REPEAT GEN_TAC THEN ASM_CASES_TAC `a = 1` THENL
   [ASM_REWRITE_TAC[ARITH; MULT_CLAUSES; ADD_CLAUSES; EXP_2] THEN
    SIMP_TAC[MULT_EQ_1; X_DEGENERATE; Y_DEGENERATE; GSYM EXISTS_REFL];
    ALL_TAC] THEN
  STRIP_TAC THEN
  SUBGOAL_THEN `?n. &x + &y * sqrt(&a pow 2 - &1) =
                    (&a + sqrt(&a pow 2 - &1)) pow n`
  MP_TAC THENL
   [UNDISCH_TAC `x EXP 2 = (a EXP 2 - 1) * y EXP 2 + 1` THEN
    SPEC_TAC(`x:num`,`x:num`) THEN SPEC_TAC(`y:num`,`y:num`) THEN
    MATCH_MP_TAC num_WF THEN X_GEN_TAC `y0:num` THEN DISCH_TAC THEN
    X_GEN_TAC `x0:num` THEN
    ASM_CASES_TAC `y0 = 0` THENL
     [ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES; ADD_CLAUSES; MULT_EQ_1] THEN
      DISCH_THEN SUBST1_TAC THEN EXISTS_TAC `0` THEN
      REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID; real_pow]; ALL_TAC] THEN
    DISCH_TAC THEN
    MP_TAC(SPECL [`a:num`; `x0:num`; `y0:num`] SOLUTIONS_INDUCTION) THEN
    ASM_REWRITE_TAC[] THEN
    DISCH_THEN(X_CHOOSE_THEN `x1:num` (X_CHOOSE_THEN `y1:num`
        STRIP_ASSUME_TAC)) THEN
    FIRST_X_ASSUM(MP_TAC o SPEC `y1:num`) THEN ASM_REWRITE_TAC[] THEN
    DISCH_THEN(MP_TAC o SPEC `x1:num`) THEN ASM_REWRITE_TAC[] THEN
    DISCH_THEN(X_CHOOSE_THEN `n:num` SUBST1_TAC) THEN
    EXISTS_TAC `SUC n` THEN REWRITE_TAC[real_pow; REAL_MUL_AC]; ALL_TAC] THEN
  ASM_SIMP_TAC[GSYM XY_POWER_POS] THEN MATCH_MP_TAC MONO_EXISTS THEN
  X_GEN_TAC `n:num` THEN
  ASM_SIMP_TAC[SQRT_LINEAR_EQ;
               ARITH_RULE `~(a = 0) /\ ~(a = 1) ==> 2 <= a`]);;
(* ------------------------------------------------------------------------- *)
(* Addition formulas.                                                        *)
(* ------------------------------------------------------------------------- *)

let ADDITION_FORMULA_POS = 
prove
 (`!a m n.
     ~(a = 0)
     ==> ((X a (m + n) = X a m * X a n + (a EXP 2 - 1) * Y a m * Y a n) /\
          (Y a (m + n) = X a m * Y a n + X a n * Y a m))`,

  REPEAT GEN_TAC THEN DISCH_TAC THEN ASM_CASES_TAC `a = 1` THENL
   [ASM_REWRITE_TAC[X_DEGENERATE; Y_DEGENERATE] THEN
    REWRITE_TAC[ARITH; MULT_CLAUSES] THEN REWRITE_TAC[ADD_AC]; ALL_TAC] THEN
  MP_TAC(SPECL [`a:num`; `m + n:num`] XY_POWER_POS) THEN
  MP_TAC(SPECL [`a:num`; `m:num`] XY_POWER_POS) THEN
  MP_TAC(SPECL [`a:num`; `n:num`] XY_POWER_POS) THEN
  ASM_REWRITE_TAC[] THEN
  REWRITE_TAC[REAL_POW_ADD] THEN
  DISCH_THEN(SUBST1_TAC o SYM) THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
  REWRITE_TAC[REAL_ARITH
   `(a + b * s) * (c + d * s) = (a  * c + (s * s) * b * d) +
                                (a * d + b * c) * s`] THEN
  ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2;  REAL_SUB_LE; REAL_POW_LE_1;
               REAL_OF_NUM_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
  SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` SUBST1_TAC THENL
   [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
    ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
                 ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
  REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_ADD] THEN
  SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` (SUBST1_TAC o SYM) THENL
   [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
    ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
                 ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
  ASM_SIMP_TAC[SQRT_LINEAR_EQ;
               ARITH_RULE `~(a = 0) /\ ~(a = 1) ==> 2 <= a`] THEN
  REWRITE_TAC[MULT_AC]);;
let ADDITION_FORMULA_NEG = 
prove
 (`!a m n.
     ~(a = 0) /\ m <= n
     ==> ((X a (n - m) = X a m * X a n - (a EXP 2 - 1) * Y a m * Y a n) /\
          (Y a (n - m) = X a m * Y a n - X a n * Y a m))`,

  REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_CASES_TAC `a = 1` THENL
   [ASM_REWRITE_TAC[X_DEGENERATE; Y_DEGENERATE] THEN
    REWRITE_TAC[ARITH; MULT_CLAUSES]; ALL_TAC] THEN
  MP_TAC(SPECL [`a:num`; `n - m:num`] XY_POWER_POS) THEN
  ASM_REWRITE_TAC[] THEN
  DISCH_THEN(MP_TAC o AP_TERM
   `( * ) (((&a - sqrt (&a pow 2 - &1)) *
            (&a + sqrt (&a pow 2 - &1))) pow m)`) THEN
  GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)
   [REAL_ARITH `(x - y) * (x + y) = x * x - y * y`] THEN
  ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2; REAL_SUB_LE;
               REAL_POW_LE_1; REAL_OF_NUM_LE;
               ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
  REWRITE_TAC[REAL_ARITH `x - (x - &1) = &1`] THEN
  REWRITE_TAC[REAL_POW_MUL; REAL_POW_ONE; REAL_MUL_LID] THEN
  REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
  REWRITE_TAC[GSYM REAL_POW_ADD] THEN
  ASM_SIMP_TAC[ARITH_RULE `m <= n ==> (m + (n - m) = n:num)`] THEN
  MP_TAC(SPECL [`a:num`; `m:num`] XY_POWER_NEG) THEN
  MP_TAC(SPECL [`a:num`; `n:num`] XY_POWER_POS) THEN
  ASM_REWRITE_TAC[] THEN
  DISCH_THEN(SUBST1_TAC o SYM) THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
  REWRITE_TAC[REAL_ARITH
   `(a - b * s) * (c + d * s) = (a * c - (s * s) * b * d) +
                                (a * d - b * c) * s`] THEN
  ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2;  REAL_SUB_LE; REAL_POW_LE_1;
               REAL_OF_NUM_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
  ONCE_REWRITE_TAC[REAL_ARITH
   `(a + b * s = (x1 - x2) + (y1 - y2) * s) =
    ((a + x2) + (b + y2) * s = x1 + y1 * s)`] THEN
  SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` SUBST1_TAC THENL
   [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
    ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
                 ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
  REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_ADD] THEN
  SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` (SUBST1_TAC o SYM) THENL
   [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
    ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
                 ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
  ASM_SIMP_TAC[SQRT_LINEAR_EQ;
               ARITH_RULE `~(a = 0) /\ ~(a = 1) ==> 2 <= a`] THEN
  DISCH_THEN(CONJUNCTS_THEN(SUBST1_TAC o SYM)) THEN
  REWRITE_TAC[MULT_AC] THEN REWRITE_TAC[ADD_SUB]);;
(* ------------------------------------------------------------------------- *)
(* Some stronger monotonicity theorems for Y.                                *)
(* ------------------------------------------------------------------------- *)

let Y_INCREASES_SUC = 
prove
 (`!a n. ~(a = 0) ==> Y a n < Y a (SUC n)`,

  REPEAT STRIP_TAC THEN ASM_SIMP_TAC[ADD1; ADDITION_FORMULA_POS] THEN
  REWRITE_TAC[X_CLAUSES; Y_CLAUSES] THEN
  MATCH_MP_TAC(ARITH_RULE `1 * y <= ay /\ ~(x = 0) ==> y < x * 1 + ay`) THEN
  ASM_SIMP_TAC[LE_MULT_RCANCEL; ARITH_RULE `1 <= a <=> ~(a = 0)`] THEN
  MATCH_MP_TAC(ARITH_RULE
    `!n. (n = 1) /\ n <= m ==> ~(m = 0)`) THEN
  EXISTS_TAC `X a 0` THEN CONJ_TAC THENL
   [REWRITE_TAC[X_CLAUSES]; ALL_TAC] THEN
  SPEC_TAC(`n:num`,`n:num`) THEN
  INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; LE_REFL] THEN
  REWRITE_TAC[ADD1] THEN ASM_MESON_TAC[LE_TRANS; X_INCREASES]);;
let Y_INCREASES_LT = 
prove
 (`!a m n. ~(a = 0) /\ m < n ==> Y a m < Y a n`,

  REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  GEN_REWRITE_TAC LAND_CONV [LT_EXISTS] THEN
  SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `d:num` THEN DISCH_TAC THEN
  MATCH_MP_TAC LTE_TRANS THEN EXISTS_TAC `Y a (SUC m)` THEN
  ASM_SIMP_TAC[Y_INCREASES_SUC] THEN
  REWRITE_TAC[ARITH_RULE `m + SUC d = SUC m + d`] THEN
  SPEC_TAC(`d:num`,`d:num`) THEN
  INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; LE_REFL] THEN
  RULE_ASSUM_TAC(REWRITE_RULE[ADD_CLAUSES]) THEN
  ASM_MESON_TAC[ADD1; LE_TRANS; Y_INCREASES]);;
let Y_INCREASES_LE = 
prove
 (`!a m n. ~(a = 0) /\ m <= n ==> Y a m <= Y a n`,

  REWRITE_TAC[LE_LT] THEN MESON_TAC[LE_REFL; Y_INCREASES_LT]);;
let Y_INJ = 
prove
 (`!a m n. ~(a = 0) ==> ((Y a m = Y a n) <=> (m = n))`,

  REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN
  MP_TAC(SPEC `a:num` Y_INCREASES_LT) THEN ASM_REWRITE_TAC[] THEN
  MESON_TAC[LT_CASES; LT_REFL]);;
(* ------------------------------------------------------------------------- *)
(* One for X (to get the same as Y, need a /= 1).                            *)
(* ------------------------------------------------------------------------- *)

let X_INCREASES_LE = 
prove
 (`!a m n. ~(a = 0) /\ m <= n ==> X a m <= X a n`,

  REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  GEN_REWRITE_TAC LAND_CONV [LE_EXISTS] THEN
  SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `d:num` THEN
  DISCH_THEN(K ALL_TAC) THEN SPEC_TAC(`d:num`,`d:num`) THEN
  INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; LE_REFL] THEN
  REWRITE_TAC[ADD1] THEN ASM_MESON_TAC[LE_TRANS; X_INCREASES]);;
let X_INCREASES_LT = 
prove
 (`!a m n. ~(a = 0) /\ ~(a = 1) /\ m < n ==> X a m < X a n`,

  REPEAT GEN_TAC THEN
  GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [GSYM LE_SUC_LT] THEN
  STRIP_TAC THEN
  MATCH_MP_TAC LTE_TRANS THEN EXISTS_TAC `X a (SUC m)` THEN
  ASM_SIMP_TAC[X_INCREASES_LE] THEN
  SPEC_TAC(`m:num`,`p:num`) THEN
  INDUCT_TAC THEN ASM_SIMP_TAC[ARITH; X_CLAUSES; ARITH_RULE
   `~(a = 0) /\ ~(a = 1) ==> 1 < a`] THEN
  REWRITE_TAC[ARITH_RULE `SUC(SUC p) = p + 2`] THEN
  REWRITE_TAC[X_CLAUSES; ADD1] THEN
  MATCH_MP_TAC(ARITH_RULE `a <= b /\ c < b ==> a < 2 * b - c`) THEN
  CONJ_TAC THENL
   [ALL_TAC;
    MATCH_MP_TAC LTE_TRANS THEN EXISTS_TAC `X a (SUC p)` THEN
    ASM_REWRITE_TAC[]] THEN
  GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = 1 * a`] THEN
  REWRITE_TAC[LE_MULT_RCANCEL; ADD1] THEN DISJ1_TAC THEN
  MAP_EVERY UNDISCH_TAC [`~(a = 0)`; `~(a = 1)`] THEN ARITH_TAC);;
let X_INCREASES_SUC = 
prove
 (`!a n. ~(a = 0) /\ ~(a = 1) ==> X a n < X a (SUC n)`,

  SIMP_TAC[X_INCREASES_LT; LT]);;
let X_INJ = 
prove
 (`!a m n. ~(a = 0) /\ ~(a = 1) ==> ((X a m = X a n) <=> (m = n))`,

  REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN
  MP_TAC(SPEC `a:num` X_INCREASES_LT) THEN ASM_REWRITE_TAC[] THEN
  MESON_TAC[LT_CASES; LT_REFL]);;
(* ------------------------------------------------------------------------- *)
(* Coprimality of "X a n" and "Y a n".                                       *)
(* ------------------------------------------------------------------------- *)

let XY_COPRIME = 
prove
 (`!a n. ~(a = 0) ==> coprime(X a n,Y a n)`,

  REPEAT GEN_TAC THEN
  DISCH_THEN(MP_TAC o SPEC `n:num` o MATCH_MP XY_ARE_SOLUTIONS) THEN
  ONCE_REWRITE_TAC[TAUT `a ==> b <=> ~b ==> ~a`] THEN
  REWRITE_TAC[coprime; NOT_FORALL_THM; LEFT_IMP_EXISTS_THM] THEN
  X_GEN_TAC `d:num` THEN REWRITE_TAC[NOT_IMP] THEN
  REWRITE_TAC[divides] THEN STRIP_TAC THEN ASM_REWRITE_TAC[EXP_2] THEN
  REWRITE_TAC[GSYM MULT_ASSOC] THEN
  GEN_REWRITE_TAC (funpow 2 RAND_CONV o LAND_CONV)
   [AC MULT_AC `a * d * x * d * x = d * d * a * x * x:num`] THEN
  DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
   `(a = b + 1) ==> (a - b = 1)`)) THEN
  ASM_REWRITE_TAC[GSYM LEFT_SUB_DISTRIB; MULT_EQ_1]);;
(* ------------------------------------------------------------------------- *)
(* Divisibility properties.                                                  *)
(* ------------------------------------------------------------------------- *)

let Y_DIVIDES_LEMMA = 
prove
 (`!a k n. ~(a = 0) ==> (Y a n) divides (Y a (n * k))`,

  REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
  ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN GEN_TAC THEN
  INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES] THEN
  REWRITE_TAC[Y_CLAUSES; DIVIDES_0] THEN
  ASM_SIMP_TAC[ADDITION_FORMULA_POS] THEN
  UNDISCH_TAC `Y a n divides Y a (n * k)` THEN
  SIMP_TAC[divides; LEFT_IMP_EXISTS_THM] THEN
  X_GEN_TAC `d:num` THEN DISCH_TAC THEN
  EXISTS_TAC `X a n * d + X a (n * k)` THEN
  REWRITE_TAC[LEFT_ADD_DISTRIB] THEN REWRITE_TAC[MULT_AC; ADD_AC]);;
let Y_DIVIDES = 
prove
 (`!a m n. ~(a = 0) ==> ((Y a m) divides (Y a n) <=> m divides n)`,

  REPEAT STRIP_TAC THEN EQ_TAC THENL
   [ALL_TAC;
    GEN_REWRITE_TAC LAND_CONV [divides] THEN
    ASM_SIMP_TAC[LEFT_IMP_EXISTS_THM; Y_DIVIDES_LEMMA]] THEN
  ONCE_REWRITE_TAC[TAUT `a ==> b <=> ~b ==> ~a`] THEN
  ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[DIVIDES_0] THEN
  ASM_CASES_TAC `m = 0` THENL
   [ASM_REWRITE_TAC[Y_CLAUSES; DIVIDES_ZERO] THEN
    MATCH_MP_TAC(ARITH_RULE
      `!n. (n = 1) /\ n <= m ==> ~(m = 0)`) THEN
    EXISTS_TAC `Y a 1` THEN CONJ_TAC THENL
     [REWRITE_TAC[Y_CLAUSES]; ALL_TAC] THEN
    ASM_SIMP_TAC[Y_INCREASES_LE; ARITH_RULE `1 <= n <=> ~(n = 0)`];
    ALL_TAC] THEN
  MP_TAC(SPECL [`n:num`; `m:num`] DIVISION) THEN
  ASM_REWRITE_TAC[] THEN
  ABBREV_TAC `q = n DIV m` THEN ABBREV_TAC `r = n MOD m` THEN
  STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
  ASM_CASES_TAC `r = 0` THEN
  ASM_SIMP_TAC[ADD_CLAUSES; DIVIDES_LMUL; DIVIDES_REFL] THEN
  DISCH_TAC THEN
  ASM_SIMP_TAC[ADDITION_FORMULA_POS] THEN
  SUBGOAL_THEN `~((Y a m) divides (X a (q * m) * Y a r))` MP_TAC THENL
   [ALL_TAC;
    REWRITE_TAC[TAUT `~a ==> ~b <=> b ==> a`] THEN DISCH_TAC THEN
    MATCH_MP_TAC DIVIDES_ADD_REVL THEN
    EXISTS_TAC `X a r * Y a (q * m)` THEN
    ASM_REWRITE_TAC[] THEN
    GEN_REWRITE_TAC (funpow 3 RAND_CONV) [MULT_SYM] THEN
    ASM_SIMP_TAC[DIVIDES_LMUL; Y_DIVIDES_LEMMA]] THEN
  DISCH_THEN(MP_TAC o MATCH_MP
   (REWRITE_RULE[IMP_CONJ] COPRIME_DIVPROD)) THEN
  REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
   [MP_TAC(SPECL [`a:num`; `q * m:num`] XY_COPRIME) THEN ASM_REWRITE_TAC[] THEN
    ONCE_REWRITE_TAC[TAUT `a ==> b <=> ~b ==> ~a`] THEN
    REWRITE_TAC[coprime; NOT_FORALL_THM; NOT_IMP] THEN
    MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:num` THEN
    STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
    ASM_MESON_TAC[DIVIDES_TRANS; Y_DIVIDES_LEMMA]; ALL_TAC] THEN
  DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN
  ASM_SIMP_TAC[DE_MORGAN_THM; NOT_LE; Y_INCREASES_LT] THEN
  ONCE_REWRITE_TAC[GSYM(CONJUNCT1 Y_CLAUSES)] THEN ASM_SIMP_TAC[Y_INJ]);;
(* ------------------------------------------------------------------------- *)
(* This lemma would be trivial from binomial theorem.                        *)
(* ------------------------------------------------------------------------- *)

let BINOMIAL_TRIVIALITY = 
prove
 (`!x y d n. ?p q.
      (&x + &y * sqrt(&d)) pow (n + 2) =
      &x pow (n + 2) +
      &(n + 2) * &x pow (n + 1) * &y * sqrt(&d) +
      &(((n + 1) * (n + 2)) DIV 2) * &x pow n * &y pow 2 * &d +
      &p * &y pow 3 + &q * &y pow 3 * sqrt(&d)`,

  GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THENL
   [REPEAT(EXISTS_TAC `0`) THEN CONV_TAC NUM_REDUCE_CONV THEN
    REWRITE_TAC[REAL_POW_1; real_pow; REAL_MUL_LZERO; REAL_ADD_RID] THEN
    REWRITE_TAC[REAL_MUL_LID] THEN REWRITE_TAC[REAL_POW_2] THEN
    REWRITE_TAC[REAL_ARITH
      `(x + y) * (x + y) = x * x + &2 * x * y + y * y`] THEN
    AP_TERM_TAC THEN AP_TERM_TAC THEN
    ONCE_REWRITE_TAC[AC REAL_MUL_AC `(a * b) * (a * b) = (a * a) * b * b`] THEN
    SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2; REAL_POS]; ALL_TAC] THEN
  GEN_REWRITE_TAC (funpow 2 BINDER_CONV o LAND_CONV o TOP_DEPTH_CONV)
    [ADD_CLAUSES; real_pow] THEN
  FIRST_ASSUM(X_CHOOSE_THEN `p:num` (X_CHOOSE_THEN `q:num` SUBST1_TAC)) THEN
  REWRITE_TAC[REAL_ARITH
   `(x + y) * (xn + xn1 + xn2 + p + q) =
    (x * xn) + (x * xn1 + y * xn) + (x * xn2 + y * xn1) +
    (y * xn2 + p * x + q * y) + (p * y + q * x)`] THEN
  ONCE_REWRITE_TAC[REAL_ARITH
   `x * n2 * xn1 * y * d + (y * d) * xn2 = (n2 * x * xn1 + xn2)  * y * d`] THEN
  REWRITE_TAC[GSYM(CONJUNCT2 real_pow)] THEN
  REWRITE_TAC[ARITH_RULE `SUC(n + m) = n + SUC m`] THEN
  REWRITE_TAC[ARITH_RULE `SUC n + m = n + SUC m`] THEN
  CONV_TAC NUM_REDUCE_CONV THEN
  REWRITE_TAC[REAL_ARITH `&n * x + x = (&n + &1) * x`] THEN
  REWRITE_TAC[REAL_OF_NUM_ADD; ARITH_RULE `(n + 2) + 1 = n + 3`] THEN
  REWRITE_TAC[GSYM REAL_ADD_ASSOC; GSYM REAL_MUL_ASSOC; REAL_EQ_LADD] THEN
  ONCE_REWRITE_TAC[REAL_ARITH
   `x * n12 * xn * y2 * d + y * s * n2 * xn1 * y * s + a =
    (n12 * (x * xn) * y2 * d + n2 * xn1 * (y * y) * (s * s)) + a`] THEN
  REWRITE_TAC[GSYM REAL_POW_2; GSYM(CONJUNCT2 real_pow)] THEN
  SIMP_TAC[SQRT_POW_2; REAL_POS] THEN
  REWRITE_TAC[ADD1; REAL_MUL_ASSOC; GSYM REAL_ADD_RDISTRIB] THEN
  SUBGOAL_THEN `&(((n + 1) * (n + 2)) DIV 2) + &(n + 2) =
                &(((n + 2) * (n + 3)) DIV 2)`
  SUBST1_TAC THENL
   [REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN
    CONV_TAC SYM_CONV THEN MATCH_MP_TAC DIV_UNIQ THEN
    EXISTS_TAC `0` THEN REWRITE_TAC[ARITH; ADD_CLAUSES] THEN
    REWRITE_TAC[ARITH_RULE `(n + 2) * (n + 3) = n * n + 5 * n + 6`] THEN
    REWRITE_TAC[ARITH_RULE
     `(x + 5 * n + 6 = (y + n + 2) * 2) <=> (x + 3 * n + 2 = 2 * y)`] THEN
    REWRITE_TAC[ARITH_RULE `n * n + 3 * n + 2 = (n + 1) * (n + 2)`] THEN
    SUBGOAL_THEN `EVEN((n + 1) * (n + 2))` MP_TAC THENL
     [REWRITE_TAC[EVEN_MULT; EVEN_ADD; ARITH_EVEN] THEN
      CONV_TAC(EQT_INTRO o TAUT); ALL_TAC] THEN
    SIMP_TAC[EVEN_EXISTS; LEFT_IMP_EXISTS_THM] THEN
    SIMP_TAC[DIV_MULT; ARITH_EQ]; ALL_TAC] THEN
  REWRITE_TAC[REAL_EQ_LADD] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
  ONCE_REWRITE_TAC[REAL_ARITH `q * y3 * s * y * s = q * y * y3 * s * s`] THEN
  SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2; REAL_POS] THEN
  ONCE_REWRITE_TAC[REAL_ARITH
   `y * s * nn * xn * y2 * d = nn * d * xn * (y * y2) * s`] THEN
  REWRITE_TAC[GSYM(CONJUNCT2 real_pow)] THEN
  EXISTS_TAC `p * x + q * y * d:num` THEN REWRITE_TAC[ARITH_SUC] THEN
  EXISTS_TAC `((n + 1) * (n + 2)) DIV 2 * d * x EXP n +
              p * y + q * x` THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD;
              GSYM REAL_OF_NUM_POW] THEN
  REWRITE_TAC[REAL_ADD_LDISTRIB; REAL_ADD_RDISTRIB] THEN
  REWRITE_TAC[REAL_MUL_AC] THEN REWRITE_TAC[REAL_ADD_AC]);;
(* ------------------------------------------------------------------------- *)
(* A lower bound theorem.                                                    *)
(* ------------------------------------------------------------------------- *)

let Y_LOWERBOUND = 
prove
 (`!a n. (2 * a - 1) EXP n <= Y a (n + 1)`,

  GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[EXP; ARITH; Y_CLAUSES] THEN
  ASM_CASES_TAC `a = 0` THEN ASM_REWRITE_TAC[ARITH; MULT_CLAUSES; LE_0] THEN
  REWRITE_TAC[ARITH_RULE `SUC n + 1 = n + 2`; Y_CLAUSES] THEN
  MATCH_MP_TAC LE_TRANS THEN
  EXISTS_TAC `(2 * a - 1) * Y a (n + 1)` THEN
  ASM_REWRITE_TAC[LE_MULT_LCANCEL] THEN
  REWRITE_TAC[RIGHT_SUB_DISTRIB; MULT_CLAUSES; GSYM MULT_ASSOC] THEN
  MATCH_MP_TAC(ARITH_RULE `a <= b ==> c - b <= c - a:num`) THEN
  ASM_SIMP_TAC[Y_INCREASES]);;
let Y_UPPERBOUND = 
prove
 (`!a n. Y a (n + 1) <= (2 * a) EXP n`,

  GEN_TAC THEN INDUCT_TAC THEN
  REWRITE_TAC[EXP; ADD_CLAUSES; Y_CLAUSES; LE_REFL] THEN
  REWRITE_TAC[ARITH_RULE `SUC(n + 1) = n + 2`; Y_CLAUSES] THEN
  MATCH_MP_TAC(ARITH_RULE `a <= b ==> a - c <= b:num`) THEN
  ASM_REWRITE_TAC[MULT_ASSOC; LE_MULT_LCANCEL]);;
(* ------------------------------------------------------------------------- *)
(* Now a key congruence.                                                     *)
(* ------------------------------------------------------------------------- *)

let XY_Y3_CONGRUENCE = 
prove
 (`!a n k. ~(a = 0)
           ==> ?q. Y a (n * k) =
                   k * (X a n) EXP (k - 1) * Y a n + q * (Y a n) EXP 3`,

  REPEAT STRIP_TAC THEN ASM_CASES_TAC `k = 0` THENL
   [EXISTS_TAC `0` THEN
    ASM_REWRITE_TAC[Y_CLAUSES; MULT_CLAUSES; ADD_CLAUSES; SUB_0]; ALL_TAC] THEN
  ASM_CASES_TAC `a = 1` THENL
   [ASM_REWRITE_TAC[X_DEGENERATE; Y_DEGENERATE; EXP_ONE] THEN
    EXISTS_TAC `0` THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
    REWRITE_TAC[MULT_AC]; ALL_TAC] THEN
  ASM_CASES_TAC `k = 1` THENL
   [ASM_REWRITE_TAC[MULT_CLAUSES; SUB_REFL; EXP] THEN
    EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES]; ALL_TAC] THEN
  MP_TAC(SPECL [`a:num`; `n * k:num`] XY_POWER_POS) THEN ASM_REWRITE_TAC[] THEN
  REWRITE_TAC[GSYM REAL_POW_POW] THEN
  MP_TAC(SPECL [`a:num`; `n:num`] XY_POWER_POS) THEN ASM_REWRITE_TAC[] THEN
  REWRITE_TAC[GSYM REAL_POW_POW] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
  SUBGOAL_THEN `2 <= k` MP_TAC THENL
   [MAP_EVERY UNDISCH_TAC [`~(k = 0)`; `~(k = 1)`] THEN ARITH_TAC;
    ALL_TAC] THEN
  GEN_REWRITE_TAC LAND_CONV [LE_EXISTS] THEN
  DISCH_THEN(X_CHOOSE_THEN `d:num`
    (SUBST1_TAC o ONCE_REWRITE_RULE[ADD_SYM])) THEN
  MP_TAC(SPECL [`X a n`; `Y a n`; `a EXP 2 - 1`; `d:num`]
               BINOMIAL_TRIVIALITY) THEN
  SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` (SUBST1_TAC o SYM) THENL
   [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
    ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
                 ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
  DISCH_THEN(X_CHOOSE_THEN `p:num` (X_CHOOSE_THEN `q:num` SUBST1_TAC)) THEN
  ONCE_REWRITE_TAC[REAL_ARITH
   `x1 + y1 + x2 + x3 + y2 = (x1 + x2 + x3) + (y1 + y2)`] THEN
  REWRITE_TAC[REAL_MUL_ASSOC; GSYM REAL_ADD_RDISTRIB] THEN
  SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` SUBST1_TAC THENL
   [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
    ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
                 ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
  REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_MUL; REAL_OF_NUM_ADD] THEN
  SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` (SUBST1_TAC o SYM) THENL
   [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
    ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
                 ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
  ASM_SIMP_TAC[SQRT_LINEAR_EQ;
               ARITH_RULE `~(p = 0) /\ ~(p = 1) ==> 2 <= p`] THEN
  DISCH_THEN(K ALL_TAC) THEN
  REWRITE_TAC[ARITH_RULE `(d + 2) - 1 = d + 1`] THEN
  EXISTS_TAC `q:num` THEN REWRITE_TAC[GSYM MULT_ASSOC]);;
(* ------------------------------------------------------------------------- *)
(* The other key divisibility result.                                        *)
(* ------------------------------------------------------------------------- *)

let Y2_DIVIDES = 
prove
 (`!a m n. ~(a = 0)
           ==> (((Y a m) EXP 2) divides (Y a n) <=> (m * Y a m) divides n)`,

  REPEAT STRIP_TAC THEN ASM_CASES_TAC `m = 0` THENL
   [ASM_REWRITE_TAC[Y_CLAUSES; MULT_CLAUSES; DIVIDES_ZERO; EXP_2] THEN
    GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM(CONJUNCT1 Y_CLAUSES)] THEN
    ASM_SIMP_TAC[Y_INJ]; ALL_TAC] THEN
  SUBGOAL_THEN `~(Y a m = 0)` ASSUME_TAC THENL
   [GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM(CONJUNCT1 Y_CLAUSES)] THEN
    ASM_SIMP_TAC[Y_INJ]; ALL_TAC] THEN
  MATCH_MP_TAC(TAUT
   `!c. (a ==> c) /\ (b ==> c) /\ (c ==> (a <=> b)) ==> (a <=> b)`) THEN
  EXISTS_TAC `m divides n` THEN REPEAT CONJ_TAC THENL
   [DISCH_TAC THEN
    SUBGOAL_THEN `(Y a m) divides (Y a n)` MP_TAC THENL
     [ALL_TAC; ASM_SIMP_TAC[Y_DIVIDES]] THEN
    UNDISCH_TAC `((Y a m) EXP 2) divides (Y a n)` THEN
    REWRITE_TAC[divides; EXP_2; GSYM MULT_ASSOC] THEN MESON_TAC[];
    REWRITE_TAC[divides; GSYM MULT_ASSOC] THEN MESON_TAC[];
    ALL_TAC] THEN
  GEN_REWRITE_TAC LAND_CONV [divides] THEN
  DISCH_THEN(X_CHOOSE_THEN `k:num` SUBST1_TAC) THEN
  MP_TAC(SPECL [`a:num`; `m:num`; `k:num`] XY_Y3_CONGRUENCE) THEN
  ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN `q:num` SUBST1_TAC) THEN
  MATCH_MP_TAC EQ_TRANS THEN
  EXISTS_TAC `((Y a m) EXP 2) divides (k * (X a m) EXP (k - 1) * Y a m)` THEN
  CONJ_TAC THENL
   [REWRITE_TAC[num_CONV `3`; EXP] THEN
    MESON_TAC[DIVIDES_ADD; DIVIDES_ADD_REVL; DIVIDES_LMUL; DIVIDES_REFL];
    ALL_TAC] THEN
  REWRITE_TAC[MULT_ASSOC] THEN
  GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [MULT_SYM] THEN
  REWRITE_TAC[EXP_2; GSYM MULT_ASSOC] THEN
  ASM_SIMP_TAC[DIVIDES_LMUL2_EQ] THEN
  EQ_TAC THEN SIMP_TAC[DIVIDES_RMUL] THEN
  DISCH_TAC THEN MATCH_MP_TAC COPRIME_DIVPROD THEN
  EXISTS_TAC `X a m EXP (k - 1)` THEN
  ONCE_REWRITE_TAC[MULT_SYM] THEN ASM_REWRITE_TAC[] THEN
  MATCH_MP_TAC COPRIME_EXP THEN
  ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_SIMP_TAC[XY_COPRIME]);;
(* ------------------------------------------------------------------------- *)
(* Some more congruences.                                                    *)
(* ------------------------------------------------------------------------- *)

let Y_N_MOD2 = 
prove
 (`!a n. ~(a = 0) ==> ?q. Y a n = 2 * q + n`,

  GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
  MATCH_MP_TAC PELL_INDUCTION THEN REWRITE_TAC[Y_CLAUSES] THEN
  REPEAT CONJ_TAC THENL
   [EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES];
    EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES];
    ALL_TAC] THEN
  REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM;
              LEFT_IMP_EXISTS_THM] THEN
  MAP_EVERY X_GEN_TAC [`n:num`; `q1:num`; `q2:num`] THEN STRIP_TAC THEN
  FIRST_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP Y_INCREASES) THEN
  ASM_REWRITE_TAC[] THEN
  REWRITE_TAC[ARITH_RULE `2 * q1 + n <= 2 * q2 + n + 1 <=> q1 <= q2`] THEN
  DISCH_TAC THEN
  EXISTS_TAC `(2 * a * q2 - q1) + (a - 1) * (n + 1)` THEN
  MATCH_MP_TAC(ARITH_RULE
    `v <= u /\ y <= x /\ (2 * (x + z) + w + v = 2 * y + u)
     ==> (u - v = 2 * ((x - y) + z) + w)`) THEN
  REPEAT CONJ_TAC THENL
   [REWRITE_TAC[LEFT_ADD_DISTRIB] THEN
    MATCH_MP_TAC(ARITH_RULE
     `x <= u /\ y <= v ==> 2 * x + y <= 2 * u + v + w`) THEN
    REWRITE_TAC[MULT_ASSOC] THEN CONJ_TAC THEN
    GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `n = 1 * n`] THENL
     [MATCH_MP_TAC LE_MULT2 THEN ASM_REWRITE_TAC[];
      REWRITE_TAC[LE_MULT_RCANCEL] THEN DISJ1_TAC] THEN
    UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC;
    REWRITE_TAC[MULT_ASSOC] THEN
    GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `n = 1 * n`] THEN
    MATCH_MP_TAC LE_MULT2 THEN ASM_REWRITE_TAC[] THEN
    UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC;
    UNDISCH_TAC `~(a = 0)` THEN SPEC_TAC(`a:num`,`a:num`) THEN
    INDUCT_TAC THEN REWRITE_TAC[NOT_SUC] THEN
    REWRITE_TAC[ARITH_RULE `SUC a - 1 = a`] THEN
    REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
    ARITH_TAC]);;
let Y_N_MODA1 = 
prove
 (`!a n. ~(a = 0) ==> ?q. Y a n = q * (a - 1) + n`,

  GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
  ASM_CASES_TAC `a = 1` THENL
   [ASM_REWRITE_TAC[SUB_REFL; Y_DEGENERATE; MULT_CLAUSES; ADD_CLAUSES];
    ALL_TAC] THEN
  MATCH_MP_TAC PELL_INDUCTION THEN REWRITE_TAC[Y_CLAUSES] THEN
  REPEAT CONJ_TAC THENL
   [EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES];
    EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES];
    ALL_TAC] THEN
  REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM;
              LEFT_IMP_EXISTS_THM] THEN
  MAP_EVERY X_GEN_TAC [`n:num`; `q1:num`; `q2:num`] THEN
  STRIP_TAC THEN
  FIRST_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP Y_INCREASES) THEN
  ASM_REWRITE_TAC[] THEN
  REWRITE_TAC[ARITH_RULE `q1 + n <= q2 + n + 1 <=> q1 <= q2 + 1`] THEN
  ASM_CASES_TAC `q2 = 0` THENL
   [ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
    REWRITE_TAC[ARITH_RULE `a <= 1 <=> (a = 0) \/ (a = 1)`] THEN
    ASM_REWRITE_TAC[MULT_EQ_0; MULT_EQ_1] THEN
    ASM_REWRITE_TAC[ARITH_RULE `(a - 1 = 0) <=> (a = 0) \/ (a = 1)`] THEN
    SIMP_TAC[ARITH_RULE `(a - 1 = 1) <=> (a = 2)`] THEN
    STRIP_TAC THEN ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THENL
     [EXISTS_TAC `2 * (n + 1)` THEN
      UNDISCH_TAC `~(a = 0)` THEN SPEC_TAC(`a:num`,`b:num`) THEN
      INDUCT_TAC THEN REWRITE_TAC[NOT_SUC] THEN
      REWRITE_TAC[ARITH_RULE `SUC n - 1 = n`] THEN
      REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
      MATCH_MP_TAC(ARITH_RULE `(a + c = b) ==> (b - a = c:num)`) THEN
      ARITH_TAC;
      REWRITE_TAC[MULT_ASSOC; ARITH] THEN
      REWRITE_TAC[ARITH_RULE `4 * (n + 1) - (1 + n) = 3 * (n + 1)`] THEN
      EXISTS_TAC `2 * n + 1` THEN ARITH_TAC];
    ALL_TAC] THEN
  DISCH_THEN(fun th ->
    EXISTS_TAC `2 * (n + 1) + 2 * a * q2 - q1` THEN MP_TAC th) THEN
  UNDISCH_TAC `~(a = 1)` THEN
  UNDISCH_TAC `~(a = 0)` THEN SPEC_TAC(`a:num`,`b:num`) THEN
  INDUCT_TAC THEN REWRITE_TAC[NOT_SUC] THEN
  REWRITE_TAC[ARITH_RULE `(SUC n = 1) <=> (n = 0)`] THEN DISCH_TAC THEN
  REWRITE_TAC[ARITH_RULE `SUC n - 1 = n`] THEN DISCH_TAC THEN
  REWRITE_TAC[RIGHT_ADD_DISTRIB; RIGHT_SUB_DISTRIB] THEN
  MATCH_MP_TAC(ARITH_RULE
    `v <= u /\ y <= x /\ (u + y = z + x + w + v)
     ==> (u - v = (z + (x - y)) + w:num)`) THEN
  REPEAT CONJ_TAC THENL
   [GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = 1 * a`] THEN
    REWRITE_TAC[MULT_ASSOC] THEN MATCH_MP_TAC LE_MULT2 THEN
    ASM_REWRITE_TAC[ARITH_RULE `q1 + n <= q2 + n + 1 <=> q1 <= q2 + 1`] THEN
    REWRITE_TAC[MULT_CLAUSES] THEN ARITH_TAC;
    MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `q2 * b + 1` THEN
    ASM_REWRITE_TAC[] THEN
    REWRITE_TAC[ARITH_RULE `a + 1 <= b <=> a < b`] THEN
    ASM_SIMP_TAC[LT_MULT_RCANCEL] THEN
    GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = 1 * a`] THEN
    REWRITE_TAC[MULT_ASSOC] THEN
    ASM_SIMP_TAC[LT_MULT_RCANCEL] THEN
    REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN ARITH_TAC;
    REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN ARITH_TAC]);;
let X_CONGRUENT = 
prove
 (`!a b c n. ~(a = 0) ==> ?q. X (a + b * c) n = X a n + q * c`,

  GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
  REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
  ASM_CASES_TAC `b * c = 0` THENL
   [GEN_TAC THEN EXISTS_TAC `0` THEN
    ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES]; ALL_TAC] THEN
  UNDISCH_TAC `~(b * c = 0)` THEN
  REWRITE_TAC[MULT_EQ_0; DE_MORGAN_THM] THEN STRIP_TAC THEN
  MATCH_MP_TAC PELL_INDUCTION THEN REWRITE_TAC[X_CLAUSES] THEN
  REPEAT CONJ_TAC THENL
   [EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES];
    EXISTS_TAC `b:num` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES];
    ALL_TAC] THEN
  REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM;
              LEFT_IMP_EXISTS_THM] THEN
  MAP_EVERY X_GEN_TAC [`n:num`; `q1:num`; `q2:num`] THEN
  STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
  REWRITE_TAC[ARITH_RULE
   `2 * (x + y) * (u + v) = 2 * x * u + 2 * u * y + 2 * (x + y) * v`] THEN
  EXISTS_TAC `(2 * X a (n + 1) * b + 2 * (a + b * c) * q2) - q1` THEN
  MATCH_MP_TAC(ARITH_RULE
   `a <= x /\ b <= y + z:num /\ ((x - a) + ((y + z) - b) = u)
    ==> ((x + y + z) - (a + b) = u)`) THEN
  REWRITE_TAC[RIGHT_SUB_DISTRIB; RIGHT_ADD_DISTRIB; GSYM MULT_ASSOC] THEN
  CONJ_TAC THENL
   [MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `1 * X a (n + 1)` THEN CONJ_TAC THENL
     [ASM_SIMP_TAC[MULT_CLAUSES; X_INCREASES]; ALL_TAC] THEN
    REWRITE_TAC[MULT_ASSOC; LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
    UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC; ALL_TAC] THEN
  MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `X (a + b * c) n` THEN CONJ_TAC THENL
   [ASM_REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] LE_ADD]; ALL_TAC] THEN
  MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `X (a + b * c) (n + 1)` THEN
  CONJ_TAC THENL [ASM_SIMP_TAC[X_INCREASES; ADD_EQ_0]; ALL_TAC] THEN
  ASM_REWRITE_TAC[] THEN MATCH_MP_TAC LE_ADD2 THEN CONJ_TAC THENL
   [GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
    GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = a * 1`] THEN
    REWRITE_TAC[GSYM MULT_ASSOC; LE_MULT_LCANCEL] THEN
    ASM_REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`; MULT_EQ_0; ARITH_EQ];
    MATCH_MP_TAC(ARITH_RULE `a <= y ==> a <= 2 * (x + y)`) THEN
    ONCE_REWRITE_TAC[AC MULT_AC `a * b * c * d = (a * b) * (c * d:num)`] THEN
    GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = 1 * a`] THEN
    REWRITE_TAC[LE_MULT_RCANCEL] THEN
    ASM_REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`; MULT_EQ_0; ARITH_EQ]]);;
let Y_CONGRUENT = 
prove
 (`!a b c n. ~(a = 0) ==> ?q. Y (a + b * c) n = Y a n + q * c`,

  GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
  REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
  ASM_CASES_TAC `b * c = 0` THENL
   [GEN_TAC THEN EXISTS_TAC `0` THEN
    ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES]; ALL_TAC] THEN
  UNDISCH_TAC `~(b * c = 0)` THEN
  REWRITE_TAC[MULT_EQ_0; DE_MORGAN_THM] THEN STRIP_TAC THEN
  MATCH_MP_TAC PELL_INDUCTION THEN REWRITE_TAC[Y_CLAUSES] THEN
  REPEAT CONJ_TAC THENL
   [EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES];
    EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES];
    ALL_TAC] THEN
  REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM;
              LEFT_IMP_EXISTS_THM] THEN
  MAP_EVERY X_GEN_TAC [`n:num`; `q1:num`; `q2:num`] THEN
  STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
  REWRITE_TAC[ARITH_RULE
   `2 * (x + y) * (u + v) = 2 * x * u + 2 * u * y + 2 * (x + y) * v`] THEN
  EXISTS_TAC `(2 * Y a (n + 1) * b + 2 * (a + b * c) * q2) - q1` THEN
  MATCH_MP_TAC(ARITH_RULE
   `a <= x /\ b <= y + z:num /\ ((x - a) + ((y + z) - b) = u)
    ==> ((x + y + z) - (a + b) = u)`) THEN
  REWRITE_TAC[RIGHT_SUB_DISTRIB; RIGHT_ADD_DISTRIB; GSYM MULT_ASSOC] THEN
  CONJ_TAC THENL
   [MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `1 * Y a (n + 1)` THEN CONJ_TAC THENL
     [ASM_SIMP_TAC[MULT_CLAUSES; Y_INCREASES]; ALL_TAC] THEN
    REWRITE_TAC[MULT_ASSOC; LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
    UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC; ALL_TAC] THEN
  MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `Y (a + b * c) n` THEN CONJ_TAC THENL
   [ASM_REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] LE_ADD]; ALL_TAC] THEN
  MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `Y (a + b * c) (n + 1)` THEN
  CONJ_TAC THENL [ASM_SIMP_TAC[Y_INCREASES; ADD_EQ_0]; ALL_TAC] THEN
  ASM_REWRITE_TAC[] THEN MATCH_MP_TAC LE_ADD2 THEN CONJ_TAC THENL
   [GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
    GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = a * 1`] THEN
    REWRITE_TAC[GSYM MULT_ASSOC; LE_MULT_LCANCEL] THEN
    ASM_REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`; MULT_EQ_0; ARITH_EQ];
    MATCH_MP_TAC(ARITH_RULE `a <= y ==> a <= 2 * (x + y)`) THEN
    ONCE_REWRITE_TAC[AC MULT_AC `a * b * c * d = (a * b) * (c * d:num)`] THEN
    GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = 1 * a`] THEN
    REWRITE_TAC[LE_MULT_RCANCEL] THEN
    ASM_REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`; MULT_EQ_0; ARITH_EQ]]);;
(* ------------------------------------------------------------------------- *)
(* A more important congruence.                                              *)
(* ------------------------------------------------------------------------- *)

let X_CONGRUENT_2NJ_POS = 
prove
 (`!a n j. ~(a = 0) ==> ?q. X a (2 * n + j) + X a j = q * X a n`,

  REPEAT STRIP_TAC THEN
  MP_TAC(SPECL [`a:num`; `n:num`; `n + j:num`] ADDITION_FORMULA_POS) THEN
  ASM_REWRITE_TAC[ARITH_RULE `n + n + j = 2 * n + j`] THEN
  DISCH_THEN(SUBST1_TAC o CONJUNCT1) THEN
  MP_TAC(SPECL [`a:num`; `n:num`; `j:num`] ADDITION_FORMULA_POS) THEN
  ASM_REWRITE_TAC[] THEN DISCH_THEN(SUBST1_TAC o CONJUNCT2) THEN
  ONCE_REWRITE_TAC[ARITH_RULE
   `(xn * a + d * yn * (xn * yj + xj * yn)) + xj =
    xn * (a + d * yn * yj) + xj * (d * yn * yn + 1)`] THEN
  ASM_SIMP_TAC[GSYM XY_ARE_SOLUTIONS; GSYM EXP_2] THEN
  REWRITE_TAC[EXP_2; ARITH_RULE
   `xn * a + xj * xn * xn = (a + xj * xn) * xn:num`] THEN
  MESON_TAC[]);;
let X_CONGRUENT_4NJ_POS = 
prove
 (`!a n j. ~(a = 0) ==> ?q. X a (4 * n + j) = q * X a n + X a j`,

  REPEAT STRIP_TAC THEN
  MP_TAC(SPECL [`a:num`; `n:num`; `2 * n + j`] X_CONGRUENT_2NJ_POS) THEN
  ASM_REWRITE_TAC[ARITH_RULE `2 * n + 2 * n + j = 4 * n + j`] THEN
  DISCH_THEN(X_CHOOSE_THEN `q1:num` MP_TAC) THEN
  DISCH_THEN(MP_TAC o C AP_THM `X a j` o AP_TERM `(+):num->num->num`) THEN
  REWRITE_TAC[GSYM ADD_ASSOC] THEN
  MP_TAC(SPECL [`a:num`; `n:num`; `j:num`] X_CONGRUENT_2NJ_POS) THEN
  ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `q2:num` MP_TAC) THEN
  DISCH_THEN SUBST1_TAC THEN
  DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
   `(y + q2 = q1 + x) ==> x <= y ==> (y = (q1 - q2) + x:num)`)) THEN
  ASM_SIMP_TAC[X_INCREASES_LE; ARITH_RULE `j <= 4 * n + j`] THEN
  DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB] THEN
  MESON_TAC[]);;
let X_CONGRUENT_4MNJ_POS = 
prove
 (`!a m n j. ~(a = 0) ==> ?q. X a (4 * m * n + j) = q * X a n + X a j`,

  GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
  DISCH_TAC THEN INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THENL
   [REPEAT GEN_TAC THEN EXISTS_TAC `0` THEN
    REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES]; ALL_TAC] THEN
  UNDISCH_TAC `!n j. ?q. X a (4 * m * n + j) = q * X a n + X a j` THEN
  REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
  DISCH_THEN(X_CHOOSE_THEN `q1:num` ASSUME_TAC) THEN
  MP_TAC(SPECL [`a:num`; `n:num`; `4 * m * n + j`] X_CONGRUENT_4NJ_POS) THEN
  ASM_REWRITE_TAC[ARITH_RULE
   `4 * (m * n + n) + j = 4 * n + 4 * m * n + j`] THEN
  DISCH_THEN(X_CHOOSE_THEN `q2:num` SUBST1_TAC) THEN
  EXISTS_TAC `q2 + q1:num` THEN ARITH_TAC);;
let X_CONGRUENT_2NJ_NEG_LEMMA = 
prove
 (`!a n j. ~(a = 0) /\ j <= n ==> ?q. X a (2 * n - j) + X a j = q * X a n`,

  REPEAT STRIP_TAC THEN ASM_CASES_TAC `j = n:num` THENL
   [EXISTS_TAC `2` THEN ASM_REWRITE_TAC[MULT_2; ADD_SUB]; ALL_TAC] THEN
  MP_TAC(SPECL [`a:num`; `n:num`; `n - j:num`] ADDITION_FORMULA_POS) THEN
  ASM_SIMP_TAC[ARITH_RULE `j <= n ==> (n + n - j = 2 * n - j)`] THEN
  STRIP_TAC THEN
  MP_TAC(SPECL [`a:num`; `j:num`; `n:num`] ADDITION_FORMULA_NEG) THEN
  ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
  EXISTS_TAC `(X a j * X a n - (a EXP 2 - 1) * Y a j * Y a n) +
              (X a j * X a n - (a EXP 2 - 1) * Y a j * Y a n)` THEN
  REWRITE_TAC[ARITH_RULE
   `((xn * a + b) + c = (a + d) * xn) <=> (b + c = xn * d:num)`] THEN
  REWRITE_TAC[LEFT_SUB_DISTRIB] THEN
  MATCH_MP_TAC(ARITH_RULE
   `b <= a /\ e <= d /\ (e + a + c = d + b)
    ==> ((a - b) + c = d - e:num)`) THEN
  REPEAT CONJ_TAC THENL
   [REWRITE_TAC[LE_MULT_LCANCEL] THEN REPEAT DISJ2_TAC THEN
    FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
     `(c = a - b) ==> 1 <= c ==> b <= a`)) THEN
    SUBST1_TAC(SYM(SPEC `a:num` (el 1 (CONJUNCTS Y_CLAUSES)))) THEN
    MATCH_MP_TAC Y_INCREASES_LE THEN
    ASM_SIMP_TAC[ARITH_RULE `j <= n ==> (1 <= n - j <=> ~(j = n))`];
    REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
    FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
     `(c = a - b) ==> 1 <= c ==> b <= a`)) THEN
    SUBST1_TAC(SYM(SPEC `a:num` (CONJUNCT1 X_CLAUSES))) THEN
    MATCH_MP_TAC X_INCREASES_LE THEN ASM_REWRITE_TAC[LE_0];
    REWRITE_TAC[ARITH_RULE
     `xn * a * yj * yn + a * yn * xj * yn + xj =
      xj * (a * yn * yn + 1) + a * yn * xn * yj`] THEN
    ASM_SIMP_TAC[GSYM XY_ARE_SOLUTIONS; GSYM EXP_2] THEN
    REWRITE_TAC[EXP_2; MULT_AC]]);;
let X_CONGRUENT_2NJ_NEG = 
prove
 (`!a n j. ~(a = 0) /\ j <= 2 * n ==> ?q. X a (2 * n - j) + X a j = q * X a n`,

  REPEAT STRIP_TAC THEN
  ASM_CASES_TAC `j <= n:num` THEN ASM_SIMP_TAC[X_CONGRUENT_2NJ_NEG_LEMMA] THEN
  MP_TAC(SPECL [`a:num`; `n:num`; `2 * n - j`] X_CONGRUENT_2NJ_NEG_LEMMA) THEN
  ASM_SIMP_TAC[ARITH_RULE `~(j <= n) ==> 2 * n - j <= n`] THEN
  ASM_SIMP_TAC[ARITH_RULE `y <= x ==> (x - (x - y) = y:num)`] THEN
  SIMP_TAC[ADD_AC]);;
(* ------------------------------------------------------------------------- *)
(* The cute GCD fact given by Smorynski.                                     *)
(* ------------------------------------------------------------------------- *)

let XY_GCD_LEMMA = 
prove
 (`!a m n. ~(a = 0) /\ m < n
           ==> (gcd(Y a m,Y a n) = Y a (gcd(m,n)))`,

  GEN_TAC THEN ASM_CASES_TAC `a = 0` THEN ASM_REWRITE_TAC[] THEN
  ASM_CASES_TAC `a = 1` THEN ASM_REWRITE_TAC[Y_DEGENERATE] THEN
  MATCH_MP_TAC num_WF THEN X_GEN_TAC `m:num` THEN DISCH_TAC THEN
  X_GEN_TAC `n:num` THEN DISCH_TAC THEN
  MP_TAC(SPECL [`n:num`; `m:num`] DIVISION) THEN
  ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[Y_CLAUSES; GCD_0] THEN
  ABBREV_TAC `q = n DIV m` THEN ABBREV_TAC `r = n MOD m` THEN
  DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `r:num`) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(MP_TAC o SPEC `m:num`) THEN ASM_REWRITE_TAC[] THEN
  MATCH_MP_TAC EQ_IMP THEN BINOP_TAC THENL
   [EXPAND_TAC "n" THEN ASM_SIMP_TAC[ADDITION_FORMULA_POS] THEN
    GEN_REWRITE_TAC LAND_CONV [GCD_SYM] THEN MATCH_MP_TAC GCD_EQ THEN
    X_GEN_TAC `d:num` THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC(TAUT
     `(a ==> (b <=> c)) ==> (a /\ b <=> a /\ c)`) THEN
    DISCH_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
    EXISTS_TAC `d divides (X a (q * m) * Y a r)` THEN CONJ_TAC THENL
     [SUBGOAL_THEN `d divides (Y a (q * m))` MP_TAC THENL
       [ASM_MESON_TAC[Y_DIVIDES; DIVIDES_TRANS; DIVIDES_LMUL; DIVIDES_REFL];
        ALL_TAC] THEN
      MESON_TAC[DIVIDES_ADD; DIVIDES_LMUL; DIVIDES_RMUL; DIVIDES_REFL;
                DIVIDES_ADD_REVL];
      ALL_TAC] THEN
    EQ_TAC THEN SIMP_TAC[DIVIDES_LMUL] THEN
    SUBGOAL_THEN `coprime(d,X a (q * m))`
     (fun th -> MESON_TAC[COPRIME_DIVPROD; th]) THEN
    SUBGOAL_THEN `d divides (Y a (q * m))` MP_TAC THENL
     [ASM_MESON_TAC[Y_DIVIDES; DIVIDES_TRANS; DIVIDES_LMUL; DIVIDES_REFL];
      ALL_TAC] THEN
    MP_TAC(SPECL [`a:num`; `q * m:num`] XY_COPRIME) THEN ASM_REWRITE_TAC[] THEN
    DISCH_TAC THEN DISCH_TAC THEN REWRITE_TAC[coprime] THEN
    X_GEN_TAC `e:num` THEN STRIP_TAC THEN
    UNDISCH_TAC `coprime (X a (q * m),Y a (q * m))` THEN
    REWRITE_TAC[coprime] THEN DISCH_THEN(MP_TAC o SPEC `e:num`) THEN
    DISCH_THEN MATCH_MP_TAC THEN ASM_MESON_TAC[DIVIDES_TRANS];
    AP_TERM_TAC THEN EXPAND_TAC "n" THEN
    GEN_REWRITE_TAC I [GSYM DIVIDES_ANTISYM] THEN
    POP_ASSUM_LIST(K ALL_TAC) THEN NUMBER_TAC]);;
let XY_GCD = 
prove
 (`!a m n. ~(a = 0) ==> (gcd(Y a m,Y a n) = Y a (gcd(m,n)))`,

  REPEAT STRIP_TAC THEN
  REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
   (SPECL [`m:num`; `n:num`] LT_CASES)
  THENL
   [ASM_SIMP_TAC[XY_GCD_LEMMA];
    ONCE_REWRITE_TAC[GCD_SYM] THEN ASM_SIMP_TAC[XY_GCD_LEMMA];
    ASM_REWRITE_TAC[GCD_REFL]]);;
(* ------------------------------------------------------------------------- *)
(* The "step-down" lemma.                                                    *)
(* ------------------------------------------------------------------------- *)

let STEP_DOWN_LEMMA = 
prove
 (`!a i j n q.
        ~(a = 0) /\ ~(a = 1) /\
        i <= j /\ j <= 2 * n /\
        (X a j = q * X a n + X a i)
        ==> (i = j) \/ ((a = 2) /\ (n = 1) /\ (i = 0) /\ (j = 2))`,

  REPEAT STRIP_TAC THEN ASM_CASES_TAC `j <= n:num` THENL
   [ASM_CASES_TAC `i = j:num` THEN ASM_REWRITE_TAC[] THEN
    SUBGOAL_THEN `i < n:num` ASSUME_TAC THENL
     [ASM_MESON_TAC[LTE_TRANS; LT_LE]; ALL_TAC] THEN
    UNDISCH_TAC `X a j = q * X a n + X a i` THEN
    ASM_CASES_TAC `q = 0` THEN
    ASM_SIMP_TAC[ADD_CLAUSES; MULT_CLAUSES; X_INJ] THEN
    DISCH_TAC THEN
    MP_TAC(SPECL [`a:num`; `j:num`; `n:num`] X_INCREASES_LE) THEN
    ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC(TAUT `~a ==> a ==> b`) THEN
    MATCH_MP_TAC(ARITH_RULE `1 <= b /\ 1 * x <= qx ==> ~(qx + b <= x)`) THEN
    SIMP_TAC[LE_MULT_RCANCEL] THEN
    ASM_SIMP_TAC[ARITH_RULE `~(x = 0) ==> 1 <= x`] THEN
    ONCE_REWRITE_TAC[GSYM(CONJUNCT1 X_CLAUSES)] THEN
    ASM_SIMP_TAC[X_INCREASES_LE; LE_0]; ALL_TAC] THEN
  ASM_CASES_TAC `n = 0` THENL
   [UNDISCH_TAC `i <= j:num` THEN UNDISCH_TAC `j <= 2 * n` THEN
    ASM_SIMP_TAC[LE; MULT_CLAUSES]; ALL_TAC] THEN
  ASM_CASES_TAC `i <= n:num` THENL
   [MP_TAC(SPECL [`a:num`; `n:num`; `j:num`] X_CONGRUENT_2NJ_NEG) THEN
    ASM_REWRITE_TAC[] THEN
    DISCH_THEN(X_CHOOSE_THEN `q1:num` MP_TAC) THEN
    UNDISCH_TAC `X a j = q * X a n + X a i` THEN
    ASM_CASES_TAC `q = 0` THEN
    ASM_SIMP_TAC[ADD_CLAUSES; MULT_CLAUSES; X_INJ] THEN DISCH_TAC THEN
    DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
     `(a + b + c = d:num) ==> (a + c = d - b)`)) THEN
    REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB] THEN
    ASM_CASES_TAC `i = n:num` THENL
     [ASM_REWRITE_TAC[] THEN
      DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
       `(x + n = q * n) ==> (x = q * n - 1 * n)`)) THEN
      MATCH_MP_TAC(TAUT `~a ==> a ==> b`) THEN
      REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB] THEN
      ASM_CASES_TAC `q1 - q - 1 = 0` THENL
       [ASM_REWRITE_TAC[MULT_CLAUSES; ARITH_RULE `~(n = 0) <=> 1 <= n`] THEN
        ONCE_REWRITE_TAC[GSYM(CONJUNCT1 X_CLAUSES)] THEN
        ASM_SIMP_TAC[X_INCREASES_LE; LE_0]; ALL_TAC] THEN
      MATCH_MP_TAC(ARITH_RULE
       `j < n /\ 1 * n <= a * n ==> ~(j = a * n)`) THEN
      ASM_SIMP_TAC[LE_MULT_RCANCEL; ARITH_RULE `~(x = 0) ==> 1 <= x`] THEN
      MATCH_MP_TAC X_INCREASES_LT THEN ASM_REWRITE_TAC[] THEN
      UNDISCH_TAC `~(j <= n:num)` THEN
      UNDISCH_TAC `~(n = 0)` THEN ARITH_TAC; ALL_TAC] THEN
    ASM_CASES_TAC `q1 - q = 0` THENL
     [ASM_REWRITE_TAC[MULT_CLAUSES; ADD_EQ_0] THEN
      MATCH_MP_TAC(TAUT `~c ==> a /\ c ==> b`) THEN
      REWRITE_TAC[ARITH_RULE `~(n = 0) <=> 1 <= n`] THEN
      ONCE_REWRITE_TAC[GSYM(CONJUNCT1 X_CLAUSES)] THEN
      ASM_SIMP_TAC[X_INCREASES_LE; LE_0]; ALL_TAC] THEN
    MATCH_MP_TAC(TAUT `(~b ==> a ==> c) ==> a ==> b \/ c`) THEN
    DISCH_TAC THEN DISCH_TAC THEN
    ASM_CASES_TAC `n = 1` THENL
     [UNDISCH_TAC `j <= 2 * n` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN
      UNDISCH_TAC `~(j <= n:num)` THEN ASM_REWRITE_TAC[] THEN
      REWRITE_TAC[IMP_IMP] THEN
      DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
       `~(j <= 1) /\ j <= 2 ==> (j = 2)`)) THEN
      DISCH_THEN SUBST_ALL_TAC THEN REWRITE_TAC[] THEN
      UNDISCH_THEN `n = 1` SUBST_ALL_TAC THEN
      SUBGOAL_THEN `i = 0` SUBST_ALL_TAC THENL
       [MAP_EVERY UNDISCH_TAC [`i <= 1`; `~(i = 1)`] THEN ARITH_TAC;
        ALL_TAC] THEN
      UNDISCH_TAC `X a (2 * 1 - 2) + X a 0 = (q1 - q) * X a 1` THEN
      REWRITE_TAC[ARITH; X_CLAUSES] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN
      MATCH_MP_TAC(ARITH_RULE
       `~(a = 0) /\ ~(a = 1) /\ a <= 2 ==> (a = 2)`) THEN
      ASM_REWRITE_TAC[] THEN
      UNDISCH_THEN `(q1 - q) * a = 2` (SUBST1_TAC o SYM) THEN
      GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = 1 * a`] THEN
      REWRITE_TAC[LE_MULT_RCANCEL] THEN
      ASM_SIMP_TAC[ARITH_RULE `~(q = 0) ==> 1 <= q`]; ALL_TAC] THEN
    UNDISCH_TAC `X a (2 * n - j) + X a i = (q1 - q) * X a n` THEN
    MATCH_MP_TAC(TAUT `~b ==> b ==> a`) THEN
    MATCH_MP_TAC(ARITH_RULE
     `s < x /\ x <= q * x ==> ~(s = q * x:num)`) THEN
    CONJ_TAC THENL
     [ALL_TAC;
      GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = 1 * a`] THEN
      REWRITE_TAC[LE_MULT_RCANCEL] THEN
      ASM_SIMP_TAC[ARITH_RULE `~(q = 0) ==> 1 <= q`]] THEN
    MATCH_MP_TAC LET_TRANS THEN
    EXISTS_TAC `2 * X a (n - 1)` THEN CONJ_TAC THENL
     [MATCH_MP_TAC(ARITH_RULE `a <= c /\ b <= c ==> a + b <= 2 * c`) THEN
      CONJ_TAC THEN MATCH_MP_TAC X_INCREASES_LE THEN ASM_REWRITE_TAC[] THENL
       [UNDISCH_TAC `~(n = 0)` THEN UNDISCH_TAC `~(j <= n:num)` THEN ARITH_TAC;
        UNDISCH_TAC `~(i = n:num)` THEN UNDISCH_TAC `i <= n:num` THEN
        ARITH_TAC];
      ALL_TAC] THEN
    SUBGOAL_THEN `n - 1 = (n - 2) + 1` SUBST1_TAC THENL
     [UNDISCH_TAC `~(n = 0)` THEN UNDISCH_TAC `~(n = 1)` THEN ARITH_TAC;
      ALL_TAC] THEN
    SUBGOAL_THEN `n = (n - 2) + 2`
     (fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [th])
    THENL
     [UNDISCH_TAC `~(n = 0)` THEN UNDISCH_TAC `~(n = 1)` THEN ARITH_TAC;
      ALL_TAC] THEN
    REWRITE_TAC[X_CLAUSES] THEN
    MATCH_MP_TAC(ARITH_RULE `z < x /\ 3 * x <= y ==> 2 * x < y - z`) THEN
    ASM_SIMP_TAC[X_INCREASES_LT; ARITH_RULE `n < n + 1`] THEN
    REWRITE_TAC[MULT_ASSOC; LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
    UNDISCH_TAC `~(a = 1)` THEN UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC;
    ALL_TAC] THEN
  MP_TAC(SPECL [`a:num`; `n:num`; `j:num`] X_CONGRUENT_2NJ_NEG) THEN
  ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN `q1:num` MP_TAC) THEN
  MP_TAC(SPECL [`a:num`; `n:num`; `i:num`] X_CONGRUENT_2NJ_NEG) THEN
  ANTS_TAC THENL
   [ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[LE_TRANS]; ALL_TAC] THEN
  DISCH_THEN(X_CHOOSE_THEN `q2:num` MP_TAC) THEN
  ASM_REWRITE_TAC[] THEN
  REWRITE_TAC[IMP_IMP] THEN
  DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
   `(a = b) /\ (c = d) ==> (a + d = b + c:num)`)) THEN
  REWRITE_TAC[ARITH_RULE
    `((x + i) + q1 = q2 + y + q3 + i) <=> (x + q1 = y + q2 + q3:num)`] THEN
  DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
   `(x + q1 = y + q2) ==> y <= x ==> (x = y + (q2 - q1:num))`)) THEN
  ANTS_TAC THENL
   [MATCH_MP_TAC X_INCREASES_LE THEN ASM_REWRITE_TAC[] THEN
    UNDISCH_TAC `i <= j:num` THEN ARITH_TAC; ALL_TAC] THEN
  REWRITE_TAC[GSYM RIGHT_ADD_DISTRIB; GSYM RIGHT_SUB_DISTRIB] THEN
  ASM_CASES_TAC `(q2 + q) - q1 = 0` THENL
   [ASM_SIMP_TAC[ADD_CLAUSES; MULT_CLAUSES; X_INJ] THEN
    MATCH_MP_TAC(TAUT `(a ==> b) ==> (a ==> b \/ c)`) THEN
    UNDISCH_TAC `j <= 2 * n` THEN UNDISCH_TAC `i <= j:num` THEN ARITH_TAC;
    ALL_TAC] THEN
  MATCH_MP_TAC(TAUT `~a ==> a ==> b`) THEN
  MATCH_MP_TAC(ARITH_RULE
   `1 * xi <= qxn /\ 1 <= xj ==> ~(xi = xj + qxn)`) THEN
  CONJ_TAC THENL
   [MATCH_MP_TAC LE_MULT2 THEN
    ASM_REWRITE_TAC[ARITH_RULE `1 <= a <=> ~(a = 0)`] THEN
    MATCH_MP_TAC X_INCREASES_LE THEN ASM_REWRITE_TAC[] THEN
    UNDISCH_TAC `~(i <= n:num)` THEN ARITH_TAC; ALL_TAC] THEN
  REWRITE_TAC[GSYM(CONJUNCT1 X_CLAUSES)] THEN
  MATCH_MP_TAC X_INCREASES_LE THEN ASM_REWRITE_TAC[LE_0]);;
let STEP_DOWN_LEMMA_4_ASYM = 
prove
 (`!a i j n q.
        ~(a = 0) /\ ~(a = 1) /\
        0 < i /\ i <= n /\ j < 4 * n /\
        (X a i + q * X a n = X a j)
        ==> (j = i) \/ (j = 4 * n - i)`,

  REPEAT STRIP_TAC THEN ASM_CASES_TAC `j <= 2 * n` THENL
   [MP_TAC(SPECL [`a:num`; `i:num`; `j:num`; `n:num`; `q:num`]
       STEP_DOWN_LEMMA) THEN
    ANTS_TAC THENL
     [ASM_REWRITE_TAC[] THEN
      UNDISCH_TAC `X a i + q * X a n = X a j` THEN
      SIMP_TAC[ADD_AC; MULT_AC] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN
      SUBGOAL_THEN `X a i <= X a j` MP_TAC THENL
       [ASM_REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] LE_ADD]; ALL_TAC] THEN
      ONCE_REWRITE_TAC[TAUT `a ==> b <=> ~b ==> ~a`] THEN
      ASM_SIMP_TAC[X_INCREASES_LT; NOT_LE]; ALL_TAC] THEN
    ASM_SIMP_TAC[ARITH_RULE `0 < i ==> ~(i = 0)`]; ALL_TAC] THEN
  DISJ_CASES_TAC(SPECL [`i:num`; `4 * n - j`] LE_CASES) THEN
  (MP_TAC(SPECL [`a:num`; `n:num`; `2 * n - (4 * n - j)`]
                X_CONGRUENT_2NJ_POS) THEN
   MP_TAC(SPECL [`a:num`; `n:num`; `4 * n - j`] X_CONGRUENT_2NJ_NEG) THEN
   ASM_SIMP_TAC[ARITH_RULE `~(j <= 2 * n) ==> 4 * n - j <= 2 * n`] THEN
   ASM_SIMP_TAC[ARITH_RULE
     `j < 4 * n /\ ~(j <= 2 * n)
      ==> (2 * n + 2 * n - (4 * n - j) = j)`] THEN
   DISCH_THEN(X_CHOOSE_THEN `q1:num` ASSUME_TAC) THEN
   DISCH_THEN(X_CHOOSE_THEN `q2:num` MP_TAC) THEN
   SUBST1_TAC(SYM(ASSUME `X a i + q * X a n = X a j`)) THEN
   UNDISCH_TAC
    `X a (2 * n - (4 * n - j)) + X a (4 * n - j) = q1 * X a n` THEN
   REWRITE_TAC[IMP_IMP] THEN
   DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
     `(a + b = c) /\ (d + a = e) ==> (b + e = c + d:num)`)))
  THENL
   [DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
     `(x + q1 = q2 + y + q3)
      ==> y <= x ==> (x = ((q2 + q3) - q1) + y:num)`));
    DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
     `(x + q1 = q2 + y + q3)
      ==> x <= y ==> (y = (q1 - (q2 + q3)) + x:num)`))] THEN
  REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB; GSYM RIGHT_ADD_DISTRIB] THEN
  ASM_SIMP_TAC[X_INCREASES_LE] THEN DISCH_TAC THENL
   [MP_TAC(SPECL [`a:num`; `i:num`; `4 * n - j`; `n:num`; `(q1 + q) - q2:num`]
      STEP_DOWN_LEMMA) THEN
    ANTS_TAC THENL
     [ASM_REWRITE_TAC[] THEN UNDISCH_TAC `~(j <= 2 * n)` THEN ARITH_TAC;
      ALL_TAC] THEN
    ASM_SIMP_TAC[ARITH_RULE `0 < i ==> ~(i = 0)`] THEN
    DISCH_TAC THEN DISJ2_TAC THEN UNDISCH_TAC `j < 4 * n` THEN ARITH_TAC;
    MP_TAC(SPECL [`a:num`; `4 * n - j`; `i:num`; `n:num`; `q2:num - (q1 + q)`]
      STEP_DOWN_LEMMA) THEN
    ANTS_TAC THENL
     [ASM_REWRITE_TAC[] THEN UNDISCH_TAC `i <= n:num` THEN ARITH_TAC;
      ALL_TAC] THEN
    ASM_REWRITE_TAC[SUB_EQ_0; GSYM NOT_LT] THEN
    DISCH_THEN(SUBST1_TAC o SYM) THEN
    DISJ2_TAC THEN UNDISCH_TAC `j < 4 * n` THEN ARITH_TAC]);;
let STEP_DOWN_LEMMA_4 = 
prove
 (`!a i j n q1 q2.
        ~(a = 0) /\ ~(a = 1) /\
        0 < i /\ i <= n /\ j < 4 * n /\
        (X a i + q1 * X a n = X a j + q2 * X a n)
        ==> (j = i) \/ (j = 4 * n - i)`,

  REPEAT STRIP_TAC THEN ASM_CASES_TAC `j < i:num` THENL
   [UNDISCH_TAC `X a i + q1 * X a n = X a j + q2 * X a n` THEN
    DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
      `(x + q1 = y + q2) ==> y < x ==> (x = y + (q2 - q1:num))`)) THEN
    ASM_SIMP_TAC[X_INCREASES_LT; GSYM RIGHT_SUB_DISTRIB] THEN
    ASM_CASES_TAC `q2 - q1 = 0` THENL
     [ASM_SIMP_TAC[MULT_CLAUSES; ADD_CLAUSES; X_INJ]; ALL_TAC] THEN
    MATCH_MP_TAC(TAUT `~a ==> a ==> b`) THEN
    DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
     `(i = j + q * n) ==> 1 <= j /\ 1 * n <= q * n ==> ~(i <= n)`)) THEN
    ASM_SIMP_TAC[X_INCREASES_LE] THEN
    ASM_SIMP_TAC[LE_MULT_RCANCEL;
                 ARITH_RULE `~(q2 - q1 = 0) ==> 1 <= q2 - q1`] THEN
    ONCE_REWRITE_TAC[GSYM(CONJUNCT1 X_CLAUSES)] THEN
    ASM_SIMP_TAC[X_INCREASES_LE; LE_0]; ALL_TAC] THEN
  MP_TAC(SPECL [`a:num`; `i:num`; `j:num`; `n:num`; `q1 - q2:num`]
               STEP_DOWN_LEMMA_4_ASYM) THEN
  DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
  REWRITE_TAC[RIGHT_SUB_DISTRIB] THEN
  MATCH_MP_TAC(ARITH_RULE
   `(i + q1 = j + q2) /\ ~(j < i) ==> (i + q1 - q2 = j:num)`) THEN
  RULE_ASSUM_TAC(REWRITE_RULE[NOT_LT]) THEN
  ASM_SIMP_TAC[NOT_LT; X_INCREASES_LE]);;
let STEP_DOWN_LEMMA_STRONG_ASYM = 
prove
 (`!a i j n c.
        ~(a = 0) /\ ~(a = 1) /\
        0 < i /\ i <= n /\
        (X a i + c * X a n = X a j)
        ==> (?q. j = i + 4 * n * q) \/
            (?q. j + i = 4 * n * q)`,

  REPEAT STRIP_TAC THEN
  MP_TAC(SPECL [`j:num`; `4 * n`] DIVISION) THEN
  ABBREV_TAC `q = j DIV (4 * n)` THEN ABBREV_TAC `k = j MOD (4 * n)` THEN
  ANTS_TAC THENL
   [UNDISCH_TAC `0 < i` THEN UNDISCH_TAC `i <= n:num` THEN ARITH_TAC;
    ALL_TAC] THEN
  DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
  MP_TAC(SPECL [`a:num`; `q:num`; `n:num`; `k:num`] X_CONGRUENT_4MNJ_POS) THEN
  ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN `q1:num` MP_TAC) THEN
  SUBST1_TAC(ARITH_RULE `4 * q * n + k = q * 4 * n + k`) THEN
  ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST_ALL_TAC THEN
  ASM_CASES_TAC `k < i:num` THENL
   [UNDISCH_TAC `X a i + c * X a n = q1 * X a n + X a k` THEN
    DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
     `(a + q1 = q2 + b) ==> b < a ==> (a = (q2 - q1) + b:num)`)) THEN
    ASM_SIMP_TAC[X_INCREASES_LT] THEN REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB] THEN
    ASM_CASES_TAC `q1 - c = 0` THENL
     [ASM_SIMP_TAC[MULT_CLAUSES; ADD_CLAUSES; X_INJ] THEN
      DISCH_TAC THEN DISJ1_TAC THEN EXISTS_TAC `q:num` THEN
      FIRST_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [SYM th]) THEN
      REWRITE_TAC[ADD_AC; MULT_AC];
      MATCH_MP_TAC(TAUT `~a ==> a ==> b`) THEN
      MATCH_MP_TAC(ARITH_RULE
       `a <= b /\ 1 <= c ==> ~(a = b + c)`) THEN
      CONJ_TAC THENL
       [GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `n = 1 * n`] THEN
        MATCH_MP_TAC LE_MULT2 THEN
        ASM_REWRITE_TAC[ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN
        ASM_SIMP_TAC[X_INCREASES_LE; LT_IMP_LE];
        SUBST1_TAC(SYM(SPEC `a:num` (CONJUNCT1 X_CLAUSES))) THEN
        ASM_SIMP_TAC[X_INCREASES_LE; LE_0]]];
    MP_TAC(SPECL [`a:num`; `i:num`; `k:num`; `n:num`; `c - q1:num`]
                 STEP_DOWN_LEMMA_4_ASYM) THEN
    ANTS_TAC THENL
     [ASM_REWRITE_TAC[] THEN
      UNDISCH_TAC `X a i + c * X a n = q1 * X a n + X a k` THEN
      DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
       `(a + q1 = q2 + b) ==> ~(b < a) ==> (a + (q1 - q2)= b:num)`)) THEN
      REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB] THEN
      DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[NOT_LT] THEN
      MATCH_MP_TAC X_INCREASES_LE THEN ASM_REWRITE_TAC[GSYM NOT_LT];
      ALL_TAC] THEN
    DISCH_THEN DISJ_CASES_TAC THENL
     [DISJ1_TAC THEN EXISTS_TAC `q:num` THEN
      UNDISCH_THEN `q * 4 * n + k = j` (SUBST1_TAC o SYM) THEN
      ASM_REWRITE_TAC[MULT_AC; ADD_AC];
      DISJ2_TAC THEN EXISTS_TAC `q + 1` THEN
      UNDISCH_THEN `q * 4 * n + k = j` (SUBST1_TAC o SYM) THEN
      REWRITE_TAC[GSYM ADD_ASSOC; LEFT_ADD_DISTRIB; MULT_CLAUSES] THEN
      ASM_REWRITE_TAC[] THEN
      MATCH_MP_TAC(ARITH_RULE
       `(a' = a) /\ i <= b ==> (a + (b - i) + i = a' + b:num)`) THEN
      REWRITE_TAC[MULT_AC] THEN
      UNDISCH_TAC `i <= n:num` THEN ARITH_TAC]]);;
let STEP_DOWN_LEMMA_STRONG = 
prove
 (`!a i j n c1 c2.
        ~(a = 0) /\ ~(a = 1) /\ 0 < i /\ i <= n /\
        (X a i + c1 * X a n = X a j + c2 * X a n)
        ==> (?q. j = i + 4 * n * q) \/
            (?q. j + i = 4 * n * q)`,

  REPEAT STRIP_TAC THEN ASM_CASES_TAC `j < i:num` THENL
   [UNDISCH_TAC `X a i + c1 * X a n = X a j + c2 * X a n` THEN
    DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
      `(x + q1 = y + q2) ==> y < x ==> (x = y + (q2 - q1:num))`)) THEN
    ASM_SIMP_TAC[X_INCREASES_LT; GSYM RIGHT_SUB_DISTRIB] THEN
    ASM_CASES_TAC `c2 - c1 = 0` THENL
     [ASM_SIMP_TAC[MULT_CLAUSES; ADD_CLAUSES; X_INJ] THEN
      DISCH_THEN(K ALL_TAC) THEN DISJ1_TAC THEN
      EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES];
      ALL_TAC] THEN
    MATCH_MP_TAC(TAUT `~a ==> a ==> b`) THEN
    DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
     `(i = j + q * n) ==> 1 <= j /\ 1 * n <= q * n ==> ~(i <= n)`)) THEN
    ASM_SIMP_TAC[X_INCREASES_LE] THEN
    ASM_SIMP_TAC[LE_MULT_RCANCEL;
                 ARITH_RULE `~(q2 - q1 = 0) ==> 1 <= q2 - q1`] THEN
    ONCE_REWRITE_TAC[GSYM(CONJUNCT1 X_CLAUSES)] THEN
    ASM_SIMP_TAC[X_INCREASES_LE; LE_0]; ALL_TAC] THEN
  MP_TAC(SPECL [`a:num`; `i:num`; `j:num`; `n:num`; `c1 - c2:num`]
               STEP_DOWN_LEMMA_STRONG_ASYM) THEN
  DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
  REWRITE_TAC[RIGHT_SUB_DISTRIB] THEN
  MATCH_MP_TAC(ARITH_RULE
   `(i + q1 = j + q2) /\ ~(j < i) ==> (i + q1 - q2 = j:num)`) THEN
  RULE_ASSUM_TAC(REWRITE_RULE[NOT_LT]) THEN
  ASM_SIMP_TAC[NOT_LT; X_INCREASES_LE]);;
(* ------------------------------------------------------------------------- *)
(* Diophantine nature of the Y sequence.                                     *)
(* ------------------------------------------------------------------------- *)

let Y_DIOPH = 
prove
 (`~(a = 0) /\ ~(a = 1) /\ ~(y = 0)
   ==> ((y = Y a k) <=>
        ?x u v r b p q s t c d.
                0 < r /\
                (x EXP 2 = (a EXP 2 - 1) * y EXP 2 + 1) /\
                (u EXP 2 = (a EXP 2 - 1) * v EXP 2 + 1) /\
                (s EXP 2 = (b EXP 2 - 1) * t EXP 2 + 1) /\
                (v = r * y EXP 2) /\
                (b = 1 + 4 * p * y) /\
                (b = a + q * u) /\
                (s = x + c * u) /\
                (t = k + 4 * d * y) /\
                k <= y)`,

  REPEAT STRIP_TAC THEN EQ_TAC THENL
   [ALL_TAC;
    DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
    MP_TAC(SPECL [`a:num`; `x:num`; `y:num`] SOLUTIONS_ARE_XY) THEN
    ASM_REWRITE_TAC[] THEN
    DISCH_THEN(X_CHOOSE_THEN `i:num` (STRIP_ASSUME_TAC o GSYM)) THEN
    MP_TAC(SPECL [`a:num`; `u:num`; `v:num`] SOLUTIONS_ARE_XY) THEN
    ASM_REWRITE_TAC[] THEN
    DISCH_THEN(X_CHOOSE_THEN `n:num` (STRIP_ASSUME_TAC o GSYM)) THEN
    SUBGOAL_THEN `~(b = 0)` ASSUME_TAC THENL
     [SUBST1_TAC(SYM(ASSUME `1 + 4 * p * y = b`)) THEN
      REWRITE_TAC[ADD_EQ_0; ARITH_EQ]; ALL_TAC] THEN
    MP_TAC(SPECL [`b:num`; `s:num`; `t:num`] SOLUTIONS_ARE_XY) THEN
    ASM_REWRITE_TAC[] THEN
    DISCH_THEN(X_CHOOSE_THEN `j:num` (STRIP_ASSUME_TAC o GSYM)) THEN
    SUBGOAL_THEN `y <= v:num` ASSUME_TAC THENL
     [SUBST1_TAC(SYM(ASSUME `r * y EXP 2 = v`)) THEN REWRITE_TAC[EXP_2] THEN
      GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `y = 1 * y`] THEN
      REWRITE_TAC[MULT_ASSOC; LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
      ASM_REWRITE_TAC[ARITH_RULE `1 <= a <=> ~(a = 0)`; MULT_EQ_0] THEN
      ASM_SIMP_TAC[ARITH_RULE `0 < r ==> ~(r = 0)`]; ALL_TAC] THEN
    SUBGOAL_THEN `i <= n:num` ASSUME_TAC THENL
     [UNDISCH_TAC `y <= v:num` THEN
      SUBST1_TAC(SYM(ASSUME `Y a i = y`)) THEN
      SUBST1_TAC(SYM(ASSUME `Y a n = v`)) THEN
      ONCE_REWRITE_TAC[TAUT `a ==> b <=> ~b ==> ~a`] THEN
      ASM_SIMP_TAC[NOT_LE; Y_INCREASES_LT]; ALL_TAC] THEN
    MP_TAC(SPECL [`a:num`; `q:num`; `u:num`; `j:num`] X_CONGRUENT) THEN
    REWRITE_TAC[ASSUME `~(a = 0)`; ASSUME `a + q * u = b:num`] THEN
    DISCH_THEN(X_CHOOSE_THEN `q1:num` MP_TAC) THEN
    SUBST1_TAC(ASSUME `X b j = s`) THEN
    SUBST1_TAC(SYM(ASSUME `x + c * u = s:num`)) THEN
    SUBST1_TAC(SYM(ASSUME `X a i = x`)) THEN
    SUBST1_TAC(SYM(ASSUME `X a n = u`)) THEN DISCH_TAC THEN
    SUBGOAL_THEN `~(i = 0)` ASSUME_TAC THENL
     [UNDISCH_TAC `~(y = 0)` THEN
      REWRITE_TAC[TAUT `~a ==> ~b <=> b ==> a`] THEN
      EXPAND_TAC "y" THEN SIMP_TAC[Y_CLAUSES; ASSUME `~(a = 0)`];
      ALL_TAC] THEN
    SUBGOAL_THEN `(?q. j = i + 4 * n * q) \/ (?q. j + i = 4 * n * q)`
    ASSUME_TAC THENL
     [MATCH_MP_TAC STEP_DOWN_LEMMA_STRONG THEN
      MAP_EVERY EXISTS_TAC [`a:num`; `c:num`; `q1:num`] THEN
      ASM_SIMP_TAC[ARITH_RULE `~(i = 0) ==> 0 < i`]; ALL_TAC] THEN
    MP_TAC(SPECL [`a:num`; `i:num`; `n:num`] Y2_DIVIDES) THEN
    ASM_REWRITE_TAC[] THEN
    DISCH_THEN(MP_TAC o fst o EQ_IMP_RULE) THEN
    REWRITE_TAC[divides; LEFT_IMP_EXISTS_THM] THEN
    DISCH_THEN(MP_TAC o SPEC `r:num`) THEN
    SUBST1_TAC(SYM(ASSUME `r * y EXP 2 = v`)) THEN
    REWRITE_TAC[EQT_INTRO(SPEC_ALL MULT_SYM)] THEN
    DISCH_THEN(X_CHOOSE_THEN `d1:num` (ASSUME_TAC o SYM)) THEN
    UNDISCH_TAC `(?q. j = i + 4 * n * q) \/ (?q. j + i = 4 * n * q:num)` THEN
    UNDISCH_THEN `(i * y) * d1 = n:num` (SUBST1_TAC o SYM) THEN DISCH_TAC THEN
    SUBGOAL_THEN `(?q. j = i + q * 4 * Y a i) \/
                  (?q. j + i = q * 4 * Y a i)`
    MP_TAC THENL
     [FIRST_ASSUM(UNDISCH_TAC o check is_disj o concl) THEN
      REWRITE_TAC[OR_EXISTS_THM] THEN
      DISCH_THEN(X_CHOOSE_THEN `d2:num`
       (fun th -> EXISTS_TAC `i * d1 * d2:num` THEN MP_TAC th)) THEN
      SUBST1_TAC(ASSUME `Y a i = y`) THEN REWRITE_TAC[MULT_AC];
      FIRST_X_ASSUM(K ALL_TAC o check (is_disj o concl)) THEN
      DISCH_TAC] THEN
    MP_TAC(SPECL [`b:num`; `j:num`] Y_N_MODA1) THEN
    ASM_REWRITE_TAC[] THEN
    DISCH_THEN(X_CHOOSE_THEN `d3:num` MP_TAC) THEN
    SUBST1_TAC(SYM(ASSUME `1 + 4 * p * y = b`)) THEN REWRITE_TAC[ADD_SUB2] THEN
    SUBST1_TAC(SYM(ASSUME `k + 4 * d * y = t`)) THEN DISCH_TAC THEN
    SUBST1_TAC(SYM(ASSUME `Y a i = y`)) THEN AP_TERM_TAC THEN
    SUBGOAL_THEN `(?q1 q2. k + q1 * 4 * Y a i = i + q2 * 4 * Y a i) \/
                  (?q. i + k = q * 4 * Y a i)`
    MP_TAC THENL
     [UNDISCH_TAC `(?q. j = i + q * 4 * Y a i) \/
                   (?q. j + i = q * 4 * Y a i)` THEN
      MATCH_MP_TAC(TAUT
       `(a1 ==> b1) /\ (a2 ==> b2) ==> a1 \/ a2 ==> b1 \/ b2`) THEN
      CONJ_TAC THEN DISCH_TAC THEN
      UNDISCH_TAC `k + 4 * d * y = d3 * 4 * p * y + j` THENL
       [FIRST_X_ASSUM(X_CHOOSE_THEN `d4:num` SUBST1_TAC) THEN
        DISCH_THEN(fun th ->
          EXISTS_TAC `d:num` THEN
          EXISTS_TAC `d3 * p + d4:num` THEN MP_TAC th) THEN
        SUBST1_TAC(SYM(ASSUME `Y a i = y`)) THEN
        REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
        REWRITE_TAC[MULT_AC] THEN REWRITE_TAC[ADD_AC];
        DISCH_THEN(MP_TAC o C AP_THM `i:num` o
          AP_TERM `(+):num->num->num`) THEN
        REWRITE_TAC[GSYM ADD_ASSOC] THEN
        FIRST_X_ASSUM(X_CHOOSE_THEN `d4:num` SUBST1_TAC) THEN
        DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
         `(k + q1 + i = q2) ==> (i + k = q2 - q1:num)`)) THEN
        DISCH_THEN SUBST1_TAC THEN
        SUBST1_TAC(SYM(ASSUME `Y a i = y`)) THEN
        REWRITE_TAC[GSYM RIGHT_ADD_DISTRIB; MULT_ASSOC;
                    GSYM RIGHT_SUB_DISTRIB] THEN
        REWRITE_TAC[GSYM MULT_ASSOC] THEN
        REWRITE_TAC[ARITH_RULE
         `(d3 * 4 * p + d4 * 4) - 4 * x =
          ((d3 * p + d4) - x) * 4`] THEN REWRITE_TAC[GSYM MULT_ASSOC] THEN
        EXISTS_TAC `(d3 * p + d4) - d:num` THEN REFL_TAC];
      ALL_TAC] THEN
    SUBGOAL_THEN `k <= Y a i` ASSUME_TAC THENL
     [ASM_REWRITE_TAC[]; ALL_TAC] THEN
    SUBGOAL_THEN `i <= Y a i` ASSUME_TAC THENL
     [MP_TAC(SPECL [`a:num`; `i:num`] Y_N_MODA1) THEN
      ASM_SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN
      REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] LE_ADD]; ALL_TAC] THEN
    DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
     [DISCH_THEN(X_CHOOSE_THEN `q4:num` (X_CHOOSE_THEN `q5:num` MP_TAC)) THEN
      REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
       (SPECL [`q4:num`; `q5:num`] LT_CASES)
      THENL
       [DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
         `(k + q4 = i + q5) ==> q4 < q5:num ==> (k = i + (q5 - q4))`)) THEN
        REWRITE_TAC[MULT_ASSOC; LT_MULT_RCANCEL; GSYM RIGHT_SUB_DISTRIB] THEN
        ASM_REWRITE_TAC[MULT_EQ_0; ARITH_EQ] THEN
        UNDISCH_TAC `k <= y:num` THEN
        MATCH_MP_TAC(TAUT `(a ==> ~b) ==> b ==> a ==> c`) THEN
        DISCH_THEN SUBST1_TAC THEN
        MATCH_MP_TAC(ARITH_RULE `1 * y < k * y ==> ~(i + k * y <= y)`) THEN
        ASM_REWRITE_TAC[LT_MULT_RCANCEL] THEN
        UNDISCH_TAC `q4 < q5:num` THEN ARITH_TAC;
        DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
         `(k + q4 = i + q5) ==> q5 < q4:num ==> (i = k + (q4 - q5))`)) THEN
        REWRITE_TAC[MULT_ASSOC; LT_MULT_RCANCEL; GSYM RIGHT_SUB_DISTRIB] THEN
        ASM_REWRITE_TAC[MULT_EQ_0; ARITH_EQ] THEN
        UNDISCH_TAC `i <= Y a i` THEN
        MATCH_MP_TAC(TAUT `(a ==> ~b) ==> b ==> a ==> c`) THEN
        ASM_REWRITE_TAC[] THEN
        DISCH_THEN SUBST1_TAC THEN
        MATCH_MP_TAC(ARITH_RULE `1 * y < k * y ==> ~(i + k * y <= y)`) THEN
        ASM_REWRITE_TAC[LT_MULT_RCANCEL] THEN
        UNDISCH_TAC `q5 < q4:num` THEN ARITH_TAC;
        ASM_SIMP_TAC[EQ_ADD_RCANCEL]];
      DISCH_THEN(X_CHOOSE_THEN `q6:num` MP_TAC) THEN
      ASM_CASES_TAC `q6 = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES; ADD_EQ_0] THEN
      UNDISCH_TAC `k <= Y a i` THEN UNDISCH_TAC `i <= Y a i` THEN
      SUBST1_TAC(ASSUME `Y a i = y`) THEN
      MATCH_MP_TAC(ARITH_RULE
       `2 * y < ay ==> i <= y ==> k <= y ==> (i + k = ay) ==> (i = k)`) THEN
      REWRITE_TAC[MULT_ASSOC; LT_MULT_RCANCEL] THEN ASM_REWRITE_TAC[] THEN
      UNDISCH_TAC `~(q6 = 0)` THEN ARITH_TAC]] THEN
  DISCH_THEN(ASSUME_TAC o SYM) THEN ABBREV_TAC `x = X a k` THEN
  SUBGOAL_THEN `x EXP 2 = (a EXP 2 - 1) * y EXP 2 + 1` (ASSUME_TAC o SYM) THENL
   [MAP_EVERY EXPAND_TAC ["x";
 "y"] THEN
    SIMP_TAC[XY_ARE_SOLUTIONS; ASSUME `~(a = 0)`]; ALL_TAC] THEN
  EXISTS_TAC `x:num` THEN ASM_REWRITE_TAC[] THEN
  ABBREV_TAC `m = 2 * k * Y a k` THEN
  ABBREV_TAC `u = X a m` THEN ABBREV_TAC `v = Y a m` THEN
  SUBGOAL_THEN `u EXP 2 = (a EXP 2 - 1) * v EXP 2 + 1` (ASSUME_TAC o SYM) THENL
   [MAP_EVERY EXPAND_TAC ["u"; "v"] THEN
    SIMP_TAC[XY_ARE_SOLUTIONS; ASSUME `~(a = 0)`]; ALL_TAC] THEN
  EXISTS_TAC `u:num` THEN EXISTS_TAC `v:num` THEN ASM_REWRITE_TAC[] THEN
  SUBGOAL_THEN `(y EXP 2) divides v` MP_TAC THENL
   [SUBST1_TAC(SYM(ASSUME `Y a m = v`)) THEN
    SUBST1_TAC(SYM(ASSUME `Y a k = y`)) THEN
    SIMP_TAC[Y2_DIVIDES; ASSUME `~(a = 0)`] THEN
    SUBST1_TAC(SYM(ASSUME `2 * k * Y a k = m`)) THEN
    REWRITE_TAC[divides] THEN EXISTS_TAC `2` THEN
    REWRITE_TAC[MULT_AC]; ALL_TAC] THEN
  REWRITE_TAC[divides] THEN
  DISCH_THEN(X_CHOOSE_THEN `r:num` (ASSUME_TAC o SYM)) THEN
  EXISTS_TAC `r:num` THEN ASM_REWRITE_TAC[] THEN
  ASM_CASES_TAC `r = 0` THENL
   [UNDISCH_TAC `y EXP 2 * r = v` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN
    DISCH_THEN(ASSUME_TAC o SYM) THEN REWRITE_TAC[LT_REFL] THEN
    UNDISCH_TAC `Y a m = v` THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
    SUBGOAL_THEN `m = 0` ASSUME_TAC THENL
     [UNDISCH_TAC `Y a m = 0` THEN
      ONCE_REWRITE_TAC[GSYM(CONJUNCT1 Y_CLAUSES)] THEN
      SIMP_TAC[Y_INJ; ASSUME `~(a = 0)`] THEN
      REWRITE_TAC[Y_CLAUSES]; ALL_TAC] THEN
    SUBGOAL_THEN `k = 0` ASSUME_TAC THENL
     [UNDISCH_TAC `2 * k * Y a k = m` THEN
      REWRITE_TAC[ASSUME `m = 0`; MULT_EQ_0; ARITH_EQ] THEN
      ONCE_REWRITE_TAC[GSYM(CONJUNCT1 Y_CLAUSES)] THEN
      SIMP_TAC[Y_INJ; ASSUME `~(a = 0)`] THEN
      REWRITE_TAC[Y_CLAUSES; EQ_SYM]; ALL_TAC] THEN
    UNDISCH_TAC `Y a k = y` THEN ASM_REWRITE_TAC[Y_CLAUSES];
    ALL_TAC] THEN
  ASM_SIMP_TAC[ARITH_RULE `~(r = 0) ==> 0 < r`] THEN
  SUBGOAL_THEN `ODD(u)` ASSUME_TAC THENL
   [UNDISCH_TAC `(a EXP 2 - 1) * v EXP 2 + 1 = u EXP 2` THEN
    DISCH_THEN(MP_TAC o AP_TERM `EVEN`) THEN
    REWRITE_TAC[EXP_2; EVEN_ADD; EVEN_MULT; ARITH_EVEN] THEN
    SUBGOAL_THEN `EVEN v` (fun th -> REWRITE_TAC[GSYM NOT_EVEN; th]) THEN
    SUBST1_TAC(SYM(ASSUME `Y a m = v`)) THEN
    MP_TAC(SPECL [`a:num`; `m:num`] Y_N_MOD2) THEN
    SIMP_TAC[ASSUME `~(a = 0)`; LEFT_IMP_EXISTS_THM] THEN
    SUBST1_TAC(SYM(ASSUME `2 * k * Y a k = m`)) THEN
    REWRITE_TAC[EVEN_ADD; EVEN_MULT; ARITH_EVEN]; ALL_TAC] THEN
  SUBGOAL_THEN `?b0 q6 q7. (b0 = 1 + q6 * 4 * y) /\ (b0 = a + q7 * u)`
  MP_TAC THENL
   [MATCH_MP_TAC CHINESE_REMAINDER THEN
    UNDISCH_TAC `ODD u` THEN
    ASM_CASES_TAC `u = 0` THEN ASM_REWRITE_TAC[ARITH_ODD] THEN
    DISCH_TAC THEN ASM_REWRITE_TAC[MULT_EQ_0; ARITH_EQ] THEN
    ONCE_REWRITE_TAC[COPRIME_SYM] THEN MATCH_MP_TAC COPRIME_MUL THEN
    CONJ_TAC THENL
     [SUBST1_TAC(SYM(NUM_REDUCE_CONV `2 * 2`)) THEN
      MATCH_MP_TAC COPRIME_MUL THEN REWRITE_TAC[] THEN
      MP_TAC(SPECL [`u:num`; `2`] PRIME_COPRIME) THEN REWRITE_TAC[PRIME_2] THEN
      MATCH_MP_TAC(TAUT `~b /\ (a ==> d) /\ (c ==> d)
                         ==> a \/ b \/ c ==> d`) THEN
      REPEAT CONJ_TAC THENL
       [UNDISCH_TAC `ODD u` THEN
        ONCE_REWRITE_TAC[TAUT `a ==> b <=> ~b ==> ~a`] THEN
        SIMP_TAC[divides; LEFT_IMP_EXISTS_THM; ODD_MULT; ARITH_ODD];
        ONCE_REWRITE_TAC[COPRIME_SYM] THEN SIMP_TAC[COPRIME_1];
        REWRITE_TAC[COPRIME_SYM]];
      MP_TAC(SPECL [`a:num`; `m:num`] XY_COPRIME) THEN ASM_REWRITE_TAC[] THEN
      SUBST1_TAC(SYM(ASSUME `y EXP 2 * r = v`)) THEN
      REWRITE_TAC[coprime; EXP_2] THEN
      MESON_TAC[DIVIDES_RMUL; DIVIDES_LMUL]]; ALL_TAC] THEN
  DISCH_THEN(X_CHOOSE_THEN `b:num` (X_CHOOSE_THEN `p:num`
        (X_CHOOSE_THEN `q:num` (STRIP_ASSUME_TAC o GSYM)))) THEN
  MAP_EVERY EXISTS_TAC [`b:num`; `p:num`; `q:num`] THEN
  ONCE_REWRITE_TAC[ARITH_RULE `1 + 4 * p * y = 1 + p * 4 * y`] THEN
  ASM_REWRITE_TAC[] THEN
  ABBREV_TAC `s = X b k` THEN ABBREV_TAC `t = Y b k` THEN
  EXISTS_TAC `s:num` THEN EXISTS_TAC `t:num` THEN
  SUBST1_TAC(ARITH_RULE `r * y EXP 2 = y EXP 2 * r`) THEN
  ASM_REWRITE_TAC[] THEN
  SUBST1_TAC(SYM(ASSUME `X b k = s`)) THEN
  SUBST1_TAC(SYM(ASSUME `Y b k = t`)) THEN
  SUBGOAL_THEN `~(b = 0)` ASSUME_TAC THENL
   [UNDISCH_THEN `1 + p * 4 * y = b` (SUBST1_TAC o SYM) THEN
    ONCE_REWRITE_TAC[TAUT `~b ==> a ==> b ==> ~a`] THEN
    REWRITE_TAC[ADD_EQ_0; ARITH_EQ]; ALL_TAC] THEN
  SIMP_TAC[XY_ARE_SOLUTIONS; ASSUME `~(b = 0)`] THEN
  MP_TAC(SPECL [`a:num`; `q:num`; `u:num`; `k:num`] X_CONGRUENT) THEN
  ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN `c:num` (ASSUME_TAC o SYM)) THEN
  EXISTS_TAC `c:num` THEN ASM_REWRITE_TAC[] THEN
  MP_TAC(SPECL [`b:num`; `k:num`] Y_N_MODA1) THEN
  SUBST1_TAC(SYM(ASSUME `1 + p * 4 * y = b`)) THEN
  REWRITE_TAC[ADD_EQ_0; ADD_SUB2; ARITH_EQ] THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN `q8:num` SUBST1_TAC) THEN
  EXISTS_TAC `q8 * p:num` THEN REWRITE_TAC[MULT_AC; ADD_AC] THEN
  MP_TAC(SPECL [`a:num`; `k:num`] Y_N_MODA1) THEN
  ASM_SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN
  REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] LE_ADD]);;

(* ------------------------------------------------------------------------- *)
(* A ratio approaches a^n for large enough k.                                *)
(* ------------------------------------------------------------------------- *)

let BINOMIALISH_LEMMA = 
prove
 (`!m n. m EXP n * (m - n) <= m * (m - 1) EXP n`,

  GEN_TAC THEN INDUCT_TAC THEN
  REWRITE_TAC[EXP; SUB_0; MULT_CLAUSES; LE_REFL] THEN
  MATCH_MP_TAC LE_TRANS THEN
  EXISTS_TAC `(m - 1) * m EXP n * (m - n)` THEN CONJ_TAC THENL
   [REWRITE_TAC[GSYM MULT_ASSOC] THEN
    ONCE_REWRITE_TAC[AC MULT_AC `a * b * c = b * a * c:num`] THEN
    REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
    REWRITE_TAC[LEFT_SUB_DISTRIB; RIGHT_SUB_DISTRIB; MULT_CLAUSES] THEN
    ONCE_REWRITE_TAC[ARITH_RULE `a - (b + c) = a - c - b:num`] THEN
    MATCH_MP_TAC(ARITH_RULE `c <= b ==> a - b <= a - c:num`) THEN ARITH_TAC;
    GEN_REWRITE_TAC RAND_CONV
     [AC MULT_AC `m * (m - 1) * n = (m - 1) * m * n`] THEN
    ASM_REWRITE_TAC[LE_MULT_LCANCEL]]);;
let XY_EXP_LEMMA = 
prove
 (`!a k n.
        ~(a = 0) /\
        2 * n * a EXP n < k
        ==> abs(&(Y (a * k) (n + 1)) / &(Y k (n + 1)) - &a pow n) < &1 / &2`,

  REPEAT STRIP_TAC THEN
  SUBGOAL_THEN `~(k = 0)` ASSUME_TAC THENL
   [FIRST_ASSUM(ACCEPT_TAC o MATCH_MP (ARITH_RULE
     `a < k ==> ~(k = 0)`)); ALL_TAC] THEN
  SUBGOAL_THEN `0 < Y k (n + 1)` ASSUME_TAC THENL
   [SUBST1_TAC(SYM(SPEC `k:num` (CONJUNCT1 Y_CLAUSES))) THEN
    ASM_SIMP_TAC[Y_INCREASES_LT; ARITH_RULE `0 < n + 1`];
    ALL_TAC] THEN
  MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN
  EXISTS_TAC `abs(&(Y k (n + 1)))` THEN
  REWRITE_TAC[GSYM REAL_ABS_MUL; REAL_SUB_LDISTRIB] THEN
  ASM_SIMP_TAC[REAL_ABS_NUM; REAL_LT_IMP_NZ;
               REAL_OF_NUM_LT; REAL_DIV_LMUL] THEN
  REWRITE_TAC[real_div; REAL_MUL_LID; REAL_MUL_ASSOC] THEN
  SIMP_TAC[GSYM real_div; REAL_OF_NUM_LT; ARITH; REAL_LT_RDIV_EQ] THEN
  MATCH_MP_TAC(REAL_ARITH
   `!lx ly ux uy.
        lx <= x /\ x <= ux /\ ly <= y /\ y <= uy /\
        &2 * uy < &2 * lx + d /\ &2 * ux < &2 * ly + d
        ==> abs(x - y) * &2 < d`) THEN
  MAP_EVERY EXISTS_TAC
   [`&((2 * a * k - 1) EXP n)`; `&((2 * k - 1) EXP n) * &a pow n`;
    `&((2 * a * k) EXP n)`; `&((2 * k) EXP n) * &a pow n`] THEN
  ASM_SIMP_TAC[REAL_OF_NUM_LE; Y_LOWERBOUND; Y_UPPERBOUND;
               REAL_LE_RMUL_EQ; REAL_POW_LT; REAL_OF_NUM_LT;
               ARITH_RULE `~(a = 0) ==> 0 < a`] THEN
  REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_POW; REAL_OF_NUM_MUL] THEN
  REWRITE_TAC[REAL_OF_NUM_LT] THEN
  MATCH_MP_TAC(ARITH_RULE
   `!x:num. x <= c /\ a < b + x /\ d < e + x ==> a < b + c /\ d < e + c`) THEN
  EXISTS_TAC `(2 * k - 1) EXP n` THEN REWRITE_TAC[Y_LOWERBOUND] THEN
  REWRITE_TAC[GSYM MULT_EXP; GSYM MULT_ASSOC] THEN
  REWRITE_TAC[RIGHT_SUB_DISTRIB; GSYM MULT_ASSOC] THEN
  SUBST1_TAC(AC MULT_AC `2 * k * a = 2 * a * k`) THEN
  REWRITE_TAC[MULT_CLAUSES] THEN
  MATCH_MP_TAC(ARITH_RULE
   `b' <= b /\ a < b' + c ==> a < b + c /\ a < b' + c:num`) THEN
  CONJ_TAC THENL
   [REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
    SPEC_TAC(`n:num`,`m:num`) THEN
    INDUCT_TAC THEN REWRITE_TAC[CONJUNCT1 EXP; LE_REFL] THEN
    REWRITE_TAC[EXP_MONO_LE_SUC] THEN UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC;
    ALL_TAC] THEN
  SUBST1_TAC(AC MULT_AC `2 * a * k = 2 * k * a`) THEN
  GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV o LAND_CONV o RAND_CONV)
   [ARITH_RULE `a = 1 * a`] THEN
  REWRITE_TAC[MULT_ASSOC; GSYM RIGHT_SUB_DISTRIB] THEN
  REWRITE_TAC[MULT_EXP] THEN
  REWRITE_TAC[ARITH_RULE `2 * e * a + e = (2 * a + 1) * e`] THEN
  REWRITE_TAC[GSYM MULT_EXP; GSYM MULT_ASSOC] THEN
  SUBST1_TAC(AC MULT_AC `2 * k * a = a * 2 * k`) THEN
  ONCE_REWRITE_TAC[MULT_EXP] THEN REWRITE_TAC[MULT_ASSOC] THEN
  SUBGOAL_THEN `(2 * k) * (2 * a EXP n) * (2 * k) EXP n <
                (2 * k) * (2 * a EXP n + 1) * (2 * k - 1) EXP n`
  MP_TAC THENL
   [ALL_TAC; ASM_SIMP_TAC[LT_MULT_LCANCEL; MULT_EQ_0; ARITH_EQ]] THEN
  GEN_REWRITE_TAC RAND_CONV
   [AC MULT_AC `(2 * k) * l * m = l * (2 * k) * m`] THEN
  MATCH_MP_TAC LTE_TRANS THEN
  EXISTS_TAC `(2 * a EXP n + 1) * (2 * k) EXP n * (2 * k - n)` THEN
  CONJ_TAC THENL
   [ALL_TAC; REWRITE_TAC[LE_MULT_LCANCEL; BINOMIALISH_LEMMA]] THEN
  REWRITE_TAC[ARITH_RULE
   `(2 * k) * (2 * an) * 2kn < a2na * 2kn * kmn <=>
    2kn * 4 * k * an < 2kn * a2na * kmn`] THEN
  ASM_SIMP_TAC[LT_MULT_LCANCEL; EXP_EQ_0; MULT_EQ_0; ARITH_EQ] THEN
  REWRITE_TAC[LEFT_SUB_DISTRIB] THEN
  MATCH_MP_TAC(ARITH_RULE `a + b < c ==> a < c - b:num`) THEN
  REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; MULT_CLAUSES] THEN
  REWRITE_TAC[GSYM MULT_ASSOC] THEN
  REWRITE_TAC[ARITH_RULE `4 * k * an + x < 2 * an * 2 * k + y <=> x < y`] THEN
  ONCE_REWRITE_TAC[AC MULT_AC `2 * a * n = 2 * n * a`] THEN
  UNDISCH_TAC `2 * n * a EXP n < k` THEN
  MATCH_MP_TAC(ARITH_RULE
   `n * 1 <= x ==> 2 * x < k ==> 2 * x + n < 2 * k`) THEN
  ASM_REWRITE_TAC[LE_MULT_LCANCEL; ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN
  ASM_REWRITE_TAC[EXP_EQ_0]);;
let ABS_LT_REPRESENTATION = 
prove
 (`!x y z.
    ~(y = 0)
    ==> (abs(&x / &y - &z) < &1 / &2 <=>
         4 * x EXP 2 + 4 * (y * z) EXP 2 < 8 * x * y * z + y EXP 2)`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
  EXISTS_TAC `&4 * (&x / &y - &z) pow 2 < &1` THEN CONJ_TAC THENL
   [SIMP_TAC[REAL_LT_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
    SUBST1_TAC(SYM(REAL_RAT_REDUCE_CONV `&2 * &2`)) THEN
    REWRITE_TAC[GSYM REAL_POW_2; GSYM REAL_POW_MUL] THEN
    ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
    REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM] THEN EQ_TAC THENL
     [GEN_REWRITE_TAC (RAND_CONV o RAND_CONV)
       [SYM(REAL_RAT_REDUCE_CONV `&1 pow 2`)] THEN
      GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN
      SIMP_TAC[ARITH_EQ; REAL_POW_LT2; REAL_LE_MUL; REAL_POS; REAL_ABS_POS];
      ONCE_REWRITE_TAC[TAUT `a ==> b <=> ~b ==> ~a`] THEN
      REWRITE_TAC[REAL_NOT_LT] THEN
      GEN_REWRITE_TAC (RAND_CONV o LAND_CONV)
       [SYM(REAL_RAT_REDUCE_CONV `&1 pow 2`)] THEN
      GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [REAL_MUL_SYM] THEN
      SIMP_TAC[ARITH_EQ; REAL_POW_LE2; REAL_LE_MUL; REAL_POS; REAL_ABS_POS]];
    ALL_TAC] THEN
  MATCH_MP_TAC EQ_TRANS THEN
  EXISTS_TAC `&4 * (&x - &y * &z) pow 2 < &y pow 2` THEN CONJ_TAC THENL
   [GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM REAL_POW2_ABS] THEN
    REWRITE_TAC[GSYM REAL_ABS_POW] THEN
    GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM REAL_MUL_LID] THEN
    ASM_SIMP_TAC[GSYM REAL_LT_LDIV_EQ; GSYM REAL_ABS_NZ; REAL_POW_EQ_0;
                 ARITH_EQ; REAL_OF_NUM_EQ] THEN
    REWRITE_TAC[REAL_ABS_POW; REAL_POW2_ABS] THEN
    REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
    REWRITE_TAC[GSYM real_div; GSYM REAL_POW_DIV] THEN
    AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
    AP_THM_TAC THEN AP_TERM_TAC THEN
    REWRITE_TAC[real_div; REAL_SUB_RDISTRIB; GSYM REAL_MUL_ASSOC] THEN
    AP_TERM_TAC THEN
    ASM_SIMP_TAC[GSYM real_div; REAL_DIV_LMUL; REAL_OF_NUM_EQ]; ALL_TAC] THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_LT; GSYM REAL_OF_NUM_ADD;
              GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_POW] THEN
  REWRITE_TAC[REAL_POW_2] THEN REAL_ARITH_TAC);;
let Y_EQ_0 = 
prove
 (`!a n. ~(a = 0) ==> ((Y a n = 0) <=> (n = 0))`,

  REPEAT STRIP_TAC THEN
  SUBST1_TAC(SYM(SPEC `a:num` (CONJUNCT1 Y_CLAUSES))) THEN
  ASM_SIMP_TAC[Y_INJ] THEN REWRITE_TAC[Y_CLAUSES]);;
let XY_EXP = 
prove
 (`~(a = 0)
   ==> ((a EXP n = p) <=>
        ?k x y z. (Y (a * k) (n + 1) = x) /\
                  (Y k (n + 1) = y) /\
                  (Y a (n + 1) = z) /\
                  2 * n * z < k /\
                  4 * x EXP 2 + 4 * (y * p) EXP 2 < 8 * x * y * p + y EXP 2)`,

  
let lemma1 = prove
   (`(?x y z. (a = x) /\ (b = y) /\ (c = z) /\ P x y z) <=> P a b c`,
    MESON_TAC[])
  and lemma2 =
    CONV_RULE(RAND_CONV(ONCE_DEPTH_CONV SYM_CONV))
             (SPEC_ALL ABS_LT_REPRESENTATION) in
  REPEAT STRIP_TAC THEN REWRITE_TAC[lemma1] THEN
  GEN_REWRITE_TAC (RAND_CONV o BINDER_CONV o LAND_CONV)
    [ARITH_RULE `n < k <=> n < k /\ ~(k = 0)`] THEN
  ONCE_REWRITE_TAC[TAUT `a /\ b <=> ~(a ==> ~b)`] THEN
  ASM_SIMP_TAC[lemma2; Y_EQ_0; ADD_EQ_0; ARITH_EQ] THEN
  REWRITE_TAC[NOT_IMP] THEN
  REWRITE_TAC[ARITH_RULE `n < k /\ ~(k = 0) <=> n < k`] THEN
  EQ_TAC THENL
   [DISCH_THEN(SUBST1_TAC o SYM) THEN
    EXISTS_TAC `2 * n * Y a (n + 1) + 1` THEN
    REWRITE_TAC[ARITH_RULE `c < c + 1`; GSYM REAL_OF_NUM_POW] THEN
    MATCH_MP_TAC XY_EXP_LEMMA THEN ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC(ARITH_RULE `a <= b ==> 2 * a < 2 * b + 1`) THEN
    REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
    MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `(2 * a - 1) EXP n` THEN
    REWRITE_TAC[Y_LOWERBOUND] THEN
    SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
    REWRITE_TAC[CONJUNCT1 EXP; LE_REFL; EXP_MONO_LE_SUC] THEN
    UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC; ALL_TAC] THEN
  DISCH_THEN(X_CHOOSE_THEN `k:num` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
  MP_TAC(SPECL [`a:num`; `k:num`; `n:num`] XY_EXP_LEMMA) THEN
  ANTS_TAC THENL
   [ASM_REWRITE_TAC[] THEN
    FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
     `2 * a < k ==> b <= a ==> 2 * b < k`)) THEN
    REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
    MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `(2 * a - 1) EXP n` THEN
    REWRITE_TAC[Y_LOWERBOUND] THEN
    SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
    REWRITE_TAC[CONJUNCT1 EXP; LE_REFL; EXP_MONO_LE_SUC] THEN
    UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC; ALL_TAC] THEN
  REWRITE_TAC[IMP_IMP] THEN
  DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
   `abs(x - a) < e1 /\ abs(x - b) < e2 ==> abs(a - b) < e1 + e2`)) THEN
  CONV_TAC REAL_RAT_REDUCE_CONV THEN
  DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
   `abs(a - b) < &1
    ==> a + &1 <= b \/ (a = b) \/ b + &1 <= a ==> (a = b)`)) THEN
  REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_ADD;
              REAL_OF_NUM_EQ; REAL_OF_NUM_LE] THEN
  DISCH_THEN MATCH_MP_TAC THEN ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Lemmas.                                                                   *)
(* ------------------------------------------------------------------------- *)

let REAL_SUM_OF_SQUARES = 
prove
 (`(x pow 2 + y pow 2 = &0) <=> (x = &0) /\ (y = &0)`,

  REWRITE_TAC[REAL_POW_2] THEN EQ_TAC THEN
  SIMP_TAC[REAL_MUL_LZERO; REAL_ADD_LID] THEN
  DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
   `(a + b = &0) ==> &0 <= a /\ &0 <= b ==> (a = &0) /\ (b = &0)`)) THEN
  REWRITE_TAC[REAL_LE_SQUARE; REAL_ENTIRE]);;
(* ------------------------------------------------------------------------- *)
(* Combining theorems for conjunction and disjunction.                       *)
(* ------------------------------------------------------------------------- *)

let DIOPH_CONJ = 
prove
 (`(x1 = x2) /\ (y1 = y2) <=>
   (x1 * x1 + x2 * x2 + y1 * y1 + y2 * y2 = 2 * x1 * x2 + 2 * y1 * y2)`,

  REWRITE_TAC[GSYM REAL_OF_NUM_EQ;
    GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL] THEN
  ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN
  REWRITE_TAC[GSYM REAL_SUM_OF_SQUARES] THEN
  REWRITE_TAC[REAL_POW_2] THEN REAL_ARITH_TAC);;
let DIOPH_DISJ = 
prove
 (`(x1 = x2) \/ (y1 = y2) <=>
   (x1 * y1 + x2 * y2 = x1 * y2 + x2 * y1)`,

  REWRITE_TAC[GSYM REAL_OF_NUM_EQ;
    GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL] THEN
  ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN
  REWRITE_TAC[GSYM REAL_ENTIRE] THEN REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Inequalities.                                                             *)
(* ------------------------------------------------------------------------- *)

let DIOPH_LE = 
prove
 (`x <= y <=> ?d:num. x + d = y`,

  REWRITE_TAC[LE_EXISTS] THEN
  AP_TERM_TAC THEN ABS_TAC THEN
  REWRITE_TAC[ADD_AC; EQ_SYM_EQ]);;
let DIOPH_LT = 
prove
 (`x < y <=> ?d. x + d + 1 = y`,

  REWRITE_TAC[LT_EXISTS] THEN
  REWRITE_TAC[ADD1] THEN
  AP_TERM_TAC THEN ABS_TAC THEN
  REWRITE_TAC[ADD_AC; EQ_SYM_EQ]);;
let DIOPH_NE = 
prove
 (`~(x = y) <=> x < y \/ y < x:num`,

  ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Exponentiation (from the Pell stuff).                                     *)
(* ------------------------------------------------------------------------- *)

let Y_0 = 
prove
 (`!k. Y 0 k = if k = 1 then 1 else 0`,

  INDUCT_TAC THEN REWRITE_TAC[Y_CLAUSES; ARITH_EQ] THEN
  SPEC_TAC(`k:num`,`k:num`) THEN
  INDUCT_TAC THEN REWRITE_TAC[Y_CLAUSES; ARITH] THEN
  REWRITE_TAC[ARITH_RULE `SUC(SUC n) = n + 2`; Y_CLAUSES; ARITH] THEN
  REWRITE_TAC[MULT_CLAUSES; SUB_0; ARITH_RULE `~(k + 2 = 1)`]);;
let Y_0_TRIV = 
prove
 (`!k. (Y 0 k = 0) <=> ~(k = 1)`,

  GEN_TAC THEN REWRITE_TAC[Y_0] THEN
  COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH_EQ]);;
let DIOPH_Y = 
prove
 (`(Y a k = y) <=>
        (a = 0) /\ (k = 1) /\ (y = 1) \/
        (a = 0) /\ ~(k = 1) /\ (y = 0) \/
        (k = 0) /\ (y = 0) \/
        (a = 1) /\ (y = k) \/
        ~(a = 0) /\ ~(k = 0) /\ ~(a = 1) /\ ~(y = 0) /\
        ?x u v r b p q s t c d.
                0 < r /\
                (x EXP 2 = (a EXP 2 - 1) * y EXP 2 + 1) /\
                (u EXP 2 = (a EXP 2 - 1) * v EXP 2 + 1) /\
                (s EXP 2 = (b EXP 2 - 1) * t EXP 2 + 1) /\
                (v = r * y EXP 2) /\
                (b = 1 + 4 * p * y) /\
                (b = a + q * u) /\
                (s = x + c * u) /\
                (t = k + 4 * d * y) /\
                k <= y`,

  ASM_CASES_TAC `a = 0` THENL
   [ASM_CASES_TAC `y = 0` THENL
     [ASM_REWRITE_TAC[Y_0_TRIV; ARITH_EQ] THEN ARITH_TAC; ALL_TAC] THEN
    ASM_CASES_TAC `k = 0` THEN ASM_REWRITE_TAC[Y_CLAUSES; ARITH_EQ] THEN
    ASM_REWRITE_TAC[ARITH_EQ] THEN CONV_TAC NUM_REDUCE_CONV THEN
    REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
    REWRITE_TAC[EXP_2; MULT_EQ_1] THEN
    REWRITE_TAC[Y_0] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
    REWRITE_TAC[EQ_SYM_EQ]; ALL_TAC] THEN
  ASM_REWRITE_TAC[ARITH_EQ] THEN
  ASM_CASES_TAC `k = 0` THEN ASM_REWRITE_TAC[Y_CLAUSES] THENL
   [REWRITE_TAC[EQ_SYM_EQ] THEN CONV_TAC(EQT_INTRO o TAUT); ALL_TAC] THEN
  ASM_CASES_TAC `a = 1` THEN ASM_REWRITE_TAC[Y_DEGENERATE] THENL
   [REWRITE_TAC[EQ_SYM_EQ]; ALL_TAC] THEN
  ASM_CASES_TAC `y = 0` THEN ASM_SIMP_TAC[Y_EQ_0] THEN
  GEN_REWRITE_TAC LAND_CONV [EQ_SYM_EQ] THEN ASM_SIMP_TAC[Y_DIOPH]);;
let DIOPH_EXP_LEMMA = 
prove
 (`(m EXP n = p) <=>
        (m = 0) /\ (n = 0) /\ (p = 1) \/
        (m = 0) /\ ~(n = 0) /\ (p = 0) \/
        ~(m = 0) /\
        ?k x y z. (Y (m * k) (n + 1) = x) /\
                  (Y k (n + 1) = y) /\
                  (Y m (n + 1) = z) /\
                  2 * n * z < k /\
                  4 * x EXP 2 + 4 * (y * p) EXP 2 < 8 * x * y * p + y EXP 2`,

  ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[ARITH_EQ] THENL
   [SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
    REWRITE_TAC[EXP; MULT_CLAUSES; ADD_CLAUSES; NOT_SUC] THEN
    REWRITE_TAC[EQ_SYM_EQ]; ALL_TAC] THEN
  ASM_SIMP_TAC[XY_EXP]);;
let DIOPH_EXP =
  let th1 = REWRITE_RULE[DIOPH_Y] DIOPH_EXP_LEMMA in
  let th2 = REWRITE_RULE[EXP_2] th1 in
  let th3 = REWRITE_RULE[DIOPH_NE; DIOPH_LT; DIOPH_LE] th2 in
  let th4 = REWRITE_RULE[ADD_CLAUSES; ARITH_EQ; ADD_EQ_0;
    ARITH_RULE `(n + 1 = 1) = (n = 0)`; ADD_ASSOC;
    EQ_ADD_RCANCEL] th3 in
  let th5 = REWRITE_RULE[GSYM ADD_ASSOC] th4 in
  REWRITE_RULE
   [OR_EXISTS_THM; LEFT_OR_EXISTS_THM; RIGHT_OR_EXISTS_THM;
    LEFT_AND_EXISTS_THM; RIGHT_AND_EXISTS_THM] th5;;

(****** This takes about an hour to compute, and longer to print out!

let DIOPH_EXP_ONE_EQUATION =
  REWRITE_RULE[DIOPH_CONJ; DIOPH_DISJ] DIOPH_EXP;;

 *******)