Examples/pell.ml

   1 (* ========================================================================= *)
   2 (* Analysis of solutions to Pell equation                                    *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/analysis.ml";;
   6 needs "Library/transc.ml";;
   7 needs "Library/prime.ml";;
   8
   9 prioritize_real();;
  10
  11 let PELL_INDUCTION = prove
  12  (`P 0 /\ P 1 /\ (!n. P n /\ P (n + 1) ==> P(n + 2)) ==> !n. P n`,
  13   STRIP_TAC THEN
  14   SUBGOAL_THEN `!n. P n /\ P(n + 1)` (fun th -> REWRITE_TAC[th]) THEN
  15   INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN
  16   ASM_SIMP_TAC[ADD1; ARITH_RULE `SUC(n + 1) = n + 2`]);;
  17
  18 (* ------------------------------------------------------------------------- *)
  19 (* Useful number-theoretic basics                                            *)
  20 (* ------------------------------------------------------------------------- *)
  21
  22 let ROOT_NONPOWER = prove
  23  (`!p q d n. ~(q = 0) /\ (p EXP n = d * q EXP n) ==> ?a. d = a EXP n`,
  24   REPEAT GEN_TAC THEN
  25   ASM_CASES_TAC `n = 0` THEN ASM_SIMP_TAC[EXP; MULT_CLAUSES] THEN
  26   STRIP_TAC THEN
  27   MP_TAC(SPECL [`n:num`; `q:num`; `p:num`] DIVIDES_EXP2_REV) THEN
  28   ASM_REWRITE_TAC[divides; LEFT_IMP_EXISTS_THM] THEN
  29   DISCH_THEN(MP_TAC o SPEC `d:num`) THEN
  30   REWRITE_TAC[EQT_INTRO(SPEC_ALL MULT_SYM)] THEN
  31   ONCE_REWRITE_TAC[MULT_SYM] THEN
  32   DISCH_THEN(X_CHOOSE_THEN `a:num` SUBST_ALL_TAC) THEN
  33   EXISTS_TAC `a:num` THEN
  34   UNDISCH_TAC `(a * q) EXP n = d * q EXP n` THEN
  35   ASM_SIMP_TAC[MULT_EXP; EQ_MULT_RCANCEL; EXP_EQ_0]);;
  36
  37 let INTEGER_SUB_LEMMA = prove
  38  (`!x y. ?n. (&x - &y) pow 2 = &n pow 2`,
  39   REPEAT STRIP_TAC THEN
  40   DISJ_CASES_THEN MP_TAC (SPECL [`&x`; `&y`] REAL_LE_TOTAL) THEN
  41   REWRITE_TAC[REAL_OF_NUM_LE] THEN DISCH_TAC THENL
  42    [EXISTS_TAC `y - x:num`; EXISTS_TAC `x - y:num`] THEN
  43   ASM_SIMP_TAC[GSYM REAL_OF_NUM_SUB] THEN
  44   REWRITE_TAC[REAL_POW_2] THEN REAL_ARITH_TAC);;
  45
  46 let SQRT_LINEAR_EQ = prove
  47  (`!a u v x y.
  48        2 <= a
  49        ==> ((&u + &v * sqrt(&a pow 2 - &1) = &x + &y * sqrt(&a pow 2 - &1)) <=>
  50             (u = x) /\ (v = y))`,
  51   REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN
  52   REWRITE_TAC[REAL_ARITH `(a + b = c + d) <=> (a - c = d - b)`] THEN
  53   REWRITE_TAC[GSYM REAL_SUB_RDISTRIB] THEN
  54   DISCH_THEN(MP_TAC o C AP_THM `2` o AP_TERM `(pow)`) THEN
  55   REWRITE_TAC[REAL_POW_MUL] THEN
  56   ASM_SIMP_TAC[SQRT_POW_2; REAL_SUB_LE; REAL_POW_LE_1; REAL_OF_NUM_LE;
  57                ARITH_RULE `2 <= a ==> 1 <= a`] THEN
  58   X_CHOOSE_TAC `p:num` (SPECL [`u:num`; `x:num`] INTEGER_SUB_LEMMA) THEN
  59   X_CHOOSE_TAC `q:num` (SPECL [`y:num`; `v:num`] INTEGER_SUB_LEMMA) THEN
  60   ASM_REWRITE_TAC[] THEN
  61   SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` SUBST1_TAC THENL
  62    [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
  63     REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
  64     ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
  65                  ARITH_RULE `2 <= a ==> 1 <= a`]; ALL_TAC] THEN
  66   REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_MUL; REAL_OF_NUM_EQ] THEN
  67   DISCH_TAC THEN
  68   MP_TAC(SPECL [`p:num`; `q:num`; `a EXP 2 - 1`; `2`] ROOT_NONPOWER) THEN
  69   ASM_REWRITE_TAC[EQT_INTRO(SPEC_ALL MULT_SYM)] THEN
  70   MATCH_MP_TAC(TAUT `~b /\ (a ==> c) ==> ((~a ==> b) ==> c)`) THEN
  71   CONJ_TAC THENL
  72    [DISCH_THEN(X_CHOOSE_THEN `b:num` MP_TAC) THEN
  73     DISCH_THEN(MP_TAC o MATCH_MP
  74      (ARITH_RULE `(a - 1 = b) ==> 1 < a ==> (a - b = 1)`)) THEN
  75     SUBST1_TAC(SYM(SPEC `a:num` (CONJUNCT1 EXP))) THEN
  76     ASM_REWRITE_TAC[LT_EXP; ARITH_LE; ARITH_LT] THEN
  77     REWRITE_TAC[EXP] THEN
  78     DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
  79       `(a - b = 1) ==> (a = b + 1)`)) THEN
  80     REWRITE_TAC[GSYM REAL_OF_NUM_EQ; GSYM REAL_OF_NUM_ADD; GSYM
  81                 REAL_OF_NUM_POW] THEN
  82     REWRITE_TAC[REAL_POW_2] THEN
  83     DISCH_THEN(MP_TAC o MATCH_MP
  84      (REAL_ARITH `(a * a = b * b + &1) ==> ((a + b) * (a - b) = &1)`)) THEN
  85     DISCH_THEN(MP_TAC o C AP_THM `2` o AP_TERM `(pow)`) THEN
  86     REWRITE_TAC[REAL_POW_MUL] THEN
  87     X_CHOOSE_TAC `c:num` (SPECL [`a:num`; `b:num`] INTEGER_SUB_LEMMA) THEN
  88     ASM_REWRITE_TAC[] THEN
  89     REWRITE_TAC[GSYM REAL_POW_MUL] THEN
  90     REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_MUL; REAL_OF_NUM_ADD] THEN
  91     REWRITE_TAC[REAL_OF_NUM_EQ; EXP_ONE; EXP_EQ_1; MULT_EQ_1; ARITH_EQ] THEN
  92     UNDISCH_TAC `2 <= a` THEN ARITH_TAC;
  93     DISCH_THEN SUBST_ALL_TAC THEN
  94     UNDISCH_TAC `p EXP 2 = 0 EXP 2 * (a EXP 2 - 1)` THEN
  95     REWRITE_TAC[ARITH; MULT_CLAUSES; EXP_EQ_0] THEN
  96     DISCH_THEN SUBST_ALL_TAC THEN
  97     UNDISCH_TAC `(&u - &x) pow 2 = &0 pow 2` THEN
  98     UNDISCH_TAC `(&y - &v) pow 2 = &0 pow 2` THEN
  99     CONV_TAC REAL_RAT_REDUCE_CONV THEN
 100     REWRITE_TAC[REAL_POW_EQ_0; ARITH_EQ; REAL_SUB_0] THEN
 101     SIMP_TAC[REAL_OF_NUM_EQ]]);;
 102
 103 (* ------------------------------------------------------------------------- *)
 104 (* Recurrence defining the solutions.                                        *)
 105 (* ------------------------------------------------------------------------- *)
 106
 107 let X_DEF =
 108   let th = prove
 109    (`!a. ?X. !n. X n = if n = 0 then 1
 110                        else if n = 1 then a
 111                        else 2 * a * X(n-1) - X(n-2)`,
 112     GEN_TAC THEN MATCH_MP_TAC(MATCH_MP WF_REC WF_num) THEN
 113     REPEAT STRIP_TAC THEN
 114     REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
 115     BINOP_TAC THEN
 116     ASM_SIMP_TAC[ARITH_RULE `n - m < n <=> ~(m = 0) /\ ~(n = 0)`; ARITH_EQ]) in
 117   new_specification ["X"] (REWRITE_RULE[SKOLEM_THM] th);;
 118
 119 let X_CLAUSES = prove
 120  (`(!a. X a 0 = 1) /\
 121    (!a. X a 1 = a) /\
 122    (!a n. X a (n + 2) = 2 * a * X a (n + 1) - X a (n))`,
 123   REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [X_DEF] THEN
 124   REWRITE_TAC[ARITH_EQ; ADD_EQ_0; ARITH_RULE `~(n + 2 = 1)`] THEN
 125   REWRITE_TAC[ARITH_RULE `((n + 2) - 2 = n) /\ ((n + 2) - 1 = n + 1)`]);;
 126
 127 let Y_DEF =
 128   let th = prove
 129    (`!a. ?Y. !n. Y n = if n = 0 then 0
 130                        else if n = 1 then 1
 131                        else 2 * a * Y(n-1) - Y(n-2)`,
 132     GEN_TAC THEN MATCH_MP_TAC(MATCH_MP WF_REC WF_num) THEN
 133     REPEAT STRIP_TAC THEN
 134     REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
 135     BINOP_TAC THEN
 136     ASM_SIMP_TAC[ARITH_RULE `n - m < n <=> ~(m = 0) /\ ~(n = 0)`; ARITH_EQ]) in
 137   new_specification ["Y"] (REWRITE_RULE[SKOLEM_THM] th);;
 138
 139 let Y_CLAUSES = prove
 140  (`(!a. Y a 0 = 0) /\
 141    (!a. Y a 1 = 1) /\
 142    (!a n. Y a (n + 2) = 2 * a * Y a (n + 1) - Y a (n))`,
 143   REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [Y_DEF] THEN
 144   REWRITE_TAC[ARITH_EQ; ADD_EQ_0; ARITH_RULE `~(n + 2 = 1)`] THEN
 145   REWRITE_TAC[ARITH_RULE `((n + 2) - 2 = n) /\ ((n + 2) - 1 = n + 1)`]);;
 146
 147 (* ------------------------------------------------------------------------- *)
 148 (* An obvious but tiresome lemma: the Xs and Ys increase.                    *)
 149 (* ------------------------------------------------------------------------- *)
 150
 151 let X_INCREASES = prove
 152  (`!a n. ~(a = 0) ==> X a n <= X a (n + 1)`,
 153   GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
 154   MATCH_MP_TAC num_WF THEN REPEAT STRIP_TAC THEN
 155   ASM_CASES_TAC `n = 0` THEN
 156   ASM_REWRITE_TAC[X_CLAUSES; ADD_CLAUSES;
 157     ARITH_RULE `1 <= a <=> ~(a = 0)`] THEN
 158   GEN_REWRITE_TAC RAND_CONV [X_DEF] THEN
 159   ASM_REWRITE_TAC[ADD_EQ_0; ARITH_EQ;
 160     ARITH_RULE `(n + 1 = 1) <=> (n = 0)`] THEN
 161   REWRITE_TAC[ADD_SUB] THEN
 162   MATCH_MP_TAC(ARITH_RULE `a + b <= c ==> a <= c - b:num`) THEN
 163   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `2 * X a n` THEN CONJ_TAC THENL
 164    [ALL_TAC;
 165     REWRITE_TAC[LE_MULT_LCANCEL; ARITH_EQ] THEN
 166     UNDISCH_TAC `~(a = 0)` THEN SPEC_TAC(`a:num`,`a:num`) THEN
 167     INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
 168     REWRITE_TAC[ARITH_RULE `a <= b + a:num`]] THEN
 169   MATCH_MP_TAC(ARITH_RULE `b <= a ==> a + b <= 2 * a`) THEN
 170   SUBGOAL_THEN `n = (n - 1) + 1` SUBST1_TAC THENL
 171    [UNDISCH_TAC `~(n = 0)` THEN ARITH_TAC; ALL_TAC] THEN
 172   REWRITE_TAC[ARITH_RULE `((n + 1) + 1) - 2 = n`] THEN
 173   FIRST_ASSUM MATCH_MP_TAC THEN
 174   UNDISCH_TAC `~(n = 0)` THEN ARITH_TAC);;
 175
 176 let Y_INCREASES = prove
 177  (`!a n. ~(a = 0) ==> Y a n <= Y a (n + 1)`,
 178   GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
 179   MATCH_MP_TAC num_WF THEN REPEAT STRIP_TAC THEN
 180   ASM_CASES_TAC `n = 0` THEN
 181   ASM_REWRITE_TAC[Y_CLAUSES; ADD_CLAUSES; LE_0] THEN
 182   GEN_REWRITE_TAC RAND_CONV [Y_DEF] THEN
 183   ASM_REWRITE_TAC[ADD_EQ_0; ARITH_EQ;
 184     ARITH_RULE `(n + 1 = 1) <=> (n = 0)`] THEN
 185   REWRITE_TAC[ADD_SUB] THEN
 186   MATCH_MP_TAC(ARITH_RULE `a + b <= c ==> a <= c - b:num`) THEN
 187   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `2 * Y a n` THEN CONJ_TAC THENL
 188    [ALL_TAC;
 189     REWRITE_TAC[LE_MULT_LCANCEL; ARITH_EQ] THEN
 190     UNDISCH_TAC `~(a = 0)` THEN SPEC_TAC(`a:num`,`a:num`) THEN
 191     INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
 192     REWRITE_TAC[ARITH_RULE `a <= b + a:num`]] THEN
 193   MATCH_MP_TAC(ARITH_RULE `b <= a ==> a + b <= 2 * a`) THEN
 194   SUBGOAL_THEN `n = (n - 1) + 1` SUBST1_TAC THENL
 195    [UNDISCH_TAC `~(n = 0)` THEN ARITH_TAC; ALL_TAC] THEN
 196   REWRITE_TAC[ARITH_RULE `((n + 1) + 1) - 2 = n`] THEN
 197   FIRST_ASSUM MATCH_MP_TAC THEN
 198   UNDISCH_TAC `~(n = 0)` THEN ARITH_TAC);;
 199
 200 (* ------------------------------------------------------------------------- *)
 201 (* Show that the expression is a power of the basis.                         *)
 202 (* ------------------------------------------------------------------------- *)
 203
 204 let XY_POWER_POS = prove
 205  (`!a n. ~(a = 0) ==> (&(X a n) + &(Y a n) * sqrt(&a pow 2 - &1) =
 206                        (&a + sqrt(&a pow 2 - &1)) pow n)`,
 207   GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
 208   MATCH_MP_TAC num_WF THEN GEN_TAC THEN DISCH_TAC THEN
 209   ONCE_REWRITE_TAC[X_DEF; Y_DEF] THEN
 210   COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH_EQ] THEN
 211   REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID; real_pow] THEN
 212   COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_POW_1; REAL_MUL_LID] THEN
 213   REWRITE_TAC[REAL_OF_NUM_ADD] THEN
 214   SUBGOAL_THEN
 215    `(&(2 * a * X a (n - 1) - X a (n - 2)) =
 216      &(2 * a * X a (n - 1)) - &(X a (n - 2))) /\
 217     (&(2 * a * Y a (n - 1) - Y a (n - 2)) =
 218      &(2 * a * Y a (n - 1)) - &(Y a (n - 2)))`
 219    (CONJUNCTS_THEN SUBST1_TAC)
 220   THENL
 221    [CONJ_TAC THEN MATCH_MP_TAC(GSYM REAL_OF_NUM_SUB) THEN
 222     MATCH_MP_TAC(ARITH_RULE
 223      `x <= y /\ y <= 2 * a * y ==> x <= 2 * a * y`) THEN
 224     ASM_SIMP_TAC[ARITH_RULE
 225      `~(n = 0) /\ ~(n = 1) ==> (n - 1 = (n - 2) + 1)`] THEN
 226     ASM_SIMP_TAC[X_INCREASES; Y_INCREASES] THEN
 227     REWRITE_TAC[MULT_ASSOC] THEN
 228     GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `n = 1 * n`] THEN
 229     REWRITE_TAC[LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
 230     UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC; ALL_TAC] THEN
 231   REWRITE_TAC[REAL_ARITH
 232    `(x1 - x2) + (y1 - y2) * a = (x1 + y1 * a) - (x2 + y2 * a)`] THEN
 233   REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
 234   REWRITE_TAC[GSYM REAL_MUL_ASSOC; GSYM REAL_ADD_LDISTRIB] THEN
 235   ASM_SIMP_TAC[ARITH_RULE
 236    `~(n = 0) /\ ~(n = 1) ==> n - 2 < n /\ n - 1 < n`] THEN
 237   ASM_SIMP_TAC[ARITH_RULE
 238      `~(n = 0) /\ ~(n = 1) ==> (n - 1 = 1 + (n - 2))`] THEN
 239   REWRITE_TAC[REAL_POW_ADD; REAL_MUL_ASSOC; REAL_POW_1] THEN
 240   REWRITE_TAC[REAL_ARITH `a * b - b = (a - &1) * b`] THEN
 241   SUBGOAL_THEN `n = 2 + (n - 2)`
 242     (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th])
 243   THENL
 244    [MAP_EVERY UNDISCH_TAC [`~(n = 0)`; `~(n = 1)`] THEN ARITH_TAC;
 245     ALL_TAC] THEN
 246   REWRITE_TAC[REAL_POW_ADD] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
 247   REWRITE_TAC[REAL_POW_2; REAL_ADD_LDISTRIB; REAL_ADD_RDISTRIB] THEN
 248   REWRITE_TAC[GSYM REAL_POW_2] THEN
 249   ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2; REAL_SUB_LE;
 250                REAL_POW_LE_1; REAL_OF_NUM_LE;
 251                ARITH_RULE `1 <= a <=> ~(a = 0)`] THEN
 252   REWRITE_TAC[REAL_POW_2] THEN REAL_ARITH_TAC);;
 253
 254 let XY_POWER_NEG = prove
 255  (`!a n. ~(a = 0) ==> (&(X a n) - &(Y a n) * sqrt(&a pow 2 - &1) =
 256                        (&a - sqrt(&a pow 2 - &1)) pow n)`,
 257   GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
 258   MATCH_MP_TAC num_WF THEN GEN_TAC THEN DISCH_TAC THEN
 259   ONCE_REWRITE_TAC[X_DEF; Y_DEF] THEN
 260   COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH_EQ] THEN
 261   REWRITE_TAC[REAL_MUL_LZERO; REAL_SUB_RZERO; real_pow] THEN
 262   COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_POW_1; REAL_MUL_LID] THEN
 263   REWRITE_TAC[REAL_OF_NUM_ADD] THEN
 264   SUBGOAL_THEN
 265    `(&(2 * a * X a (n - 1) - X a (n - 2)) =
 266      &(2 * a * X a (n - 1)) - &(X a (n - 2))) /\
 267     (&(2 * a * Y a (n - 1) - Y a (n - 2)) =
 268      &(2 * a * Y a (n - 1)) - &(Y a (n - 2)))`
 269    (CONJUNCTS_THEN SUBST1_TAC)
 270   THENL
 271    [CONJ_TAC THEN MATCH_MP_TAC(GSYM REAL_OF_NUM_SUB) THEN
 272     MATCH_MP_TAC(ARITH_RULE
 273      `x <= y /\ y <= 2 * a * y ==> x <= 2 * a * y`) THEN
 274     ASM_SIMP_TAC[ARITH_RULE
 275      `~(n = 0) /\ ~(n = 1) ==> (n - 1 = (n - 2) + 1)`] THEN
 276     ASM_SIMP_TAC[X_INCREASES; Y_INCREASES] THEN
 277     REWRITE_TAC[MULT_ASSOC] THEN
 278     GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `n = 1 * n`] THEN
 279     REWRITE_TAC[LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
 280     UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC; ALL_TAC] THEN
 281   REWRITE_TAC[REAL_ARITH
 282    `(x1 - x2) - (y1 - y2) * a = (x1 - y1 * a) - (x2 - y2 * a)`] THEN
 283   REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
 284   REWRITE_TAC[GSYM REAL_MUL_ASSOC; GSYM REAL_SUB_LDISTRIB] THEN
 285   ASM_SIMP_TAC[ARITH_RULE
 286    `~(n = 0) /\ ~(n = 1) ==> n - 2 < n /\ n - 1 < n`] THEN
 287   ASM_SIMP_TAC[ARITH_RULE
 288      `~(n = 0) /\ ~(n = 1) ==> (n - 1 = 1 + (n - 2))`] THEN
 289   REWRITE_TAC[REAL_POW_ADD; REAL_MUL_ASSOC; REAL_POW_1] THEN
 290   REWRITE_TAC[REAL_ARITH `a * b - b = (a - &1) * b`] THEN
 291   SUBGOAL_THEN `n = 2 + (n - 2)`
 292     (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th])
 293   THENL
 294    [MAP_EVERY UNDISCH_TAC [`~(n = 0)`; `~(n = 1)`] THEN ARITH_TAC;
 295     ALL_TAC] THEN
 296   REWRITE_TAC[REAL_POW_ADD] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
 297   REWRITE_TAC[REAL_POW_2; REAL_SUB_LDISTRIB; REAL_SUB_RDISTRIB] THEN
 298   REWRITE_TAC[GSYM REAL_POW_2] THEN
 299   ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2; REAL_SUB_LE;
 300                REAL_POW_LE_1; REAL_OF_NUM_LE;
 301                ARITH_RULE `1 <= a <=> ~(a = 0)`] THEN
 302   REWRITE_TAC[REAL_POW_2] THEN REAL_ARITH_TAC);;
 303
 304 (* ------------------------------------------------------------------------- *)
 305 (* Hence all members of recurrence relations are Pell solutions.             *)
 306 (* ------------------------------------------------------------------------- *)
 307
 308 let XY_ARE_SOLUTIONS = prove
 309  (`!a n. ~(a = 0)
 310          ==> ((X a n) EXP 2 = (a EXP 2 - 1) * (Y a n) EXP 2 + 1)`,
 311   REPEAT STRIP_TAC THEN
 312   FIRST_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP XY_POWER_NEG) THEN
 313   FIRST_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP XY_POWER_POS) THEN
 314   REWRITE_TAC[IMP_IMP] THEN
 315   DISCH_THEN(fun th ->
 316    MP_TAC(MK_COMB(AP_TERM `( * )` (CONJUNCT1 th),CONJUNCT2 th))) THEN
 317   REWRITE_TAC[GSYM REAL_POW_MUL] THEN
 318   REWRITE_TAC[REAL_ARITH `(x + y) * (x - y) = x * x - y * y`] THEN
 319   ONCE_REWRITE_TAC[AC REAL_MUL_AC
 320     `(a * b) * (c * d) = (a * c) * (b * d)`] THEN
 321   ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2; REAL_SUB_LE;
 322                REAL_POW_LE_1; REAL_OF_NUM_LE;
 323                ARITH_RULE `1 <= a <=> ~(a = 0)`] THEN
 324   REWRITE_TAC[REAL_ARITH `a - (a - &1) = &1`; REAL_POW_ONE] THEN
 325   REWRITE_TAC[REAL_EQ_SUB_RADD] THEN
 326   SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` SUBST1_TAC THENL
 327    [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
 328     REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
 329     ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
 330                  ARITH_RULE `1 <= a <=> ~(a = 0)`];
 331     REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_MUL; REAL_OF_NUM_EQ;
 332                 REAL_OF_NUM_POW] THEN
 333     REWRITE_TAC[MULT_AC; ADD_AC]]);;
 334
 335 (* ------------------------------------------------------------------------- *)
 336 (* And they are all solutions.                                               *)
 337 (* ------------------------------------------------------------------------- *)
 338
 339 let X_DEGENERATE = prove
 340  (`!n. X 1 n = 1`,
 341   MATCH_MP_TAC PELL_INDUCTION THEN SIMP_TAC[X_CLAUSES; ARITH]);;
 342
 343 let Y_DEGENERATE = prove
 344  (`!n. Y 1 n = n`,
 345   MATCH_MP_TAC PELL_INDUCTION THEN SIMP_TAC[Y_CLAUSES] THEN
 346   REPEAT STRIP_TAC THEN ARITH_TAC);;
 347
 348 let REAL_ARCH_POW = prove
 349  (`!x y. &1 < x /\ &1 < y
 350          ==> ?n. x pow n <= y /\ y < x pow (SUC n)`,
 351   REPEAT STRIP_TAC THEN
 352   MP_TAC(SPEC `ln(x)` REAL_ARCH_LEAST) THEN ASM_SIMP_TAC[LN_POS_LT] THEN
 353   DISCH_THEN(MP_TAC o SPEC `ln(y)`) THEN
 354   ASM_SIMP_TAC[LN_POS_LT; REAL_LT_IMP_LE] THEN
 355   ASM_SIMP_TAC[GSYM LN_POW; REAL_ARITH `&1 < x ==> &0 < x`;
 356                REAL_POW_LT; LN_MONO_LT; LN_MONO_LE]);;
 357
 358 let SOLUTIONS_INDUCTION = prove
 359  (`!a x y.
 360         ~(a = 0) /\ ~(a = 1) /\ ~(y = 0) /\
 361         (x EXP 2 = (a EXP 2 - 1) * y EXP 2 + 1)
 362         ==> ?x' y'. x' < x /\ y' < y /\
 363                     (x' EXP 2 = (a EXP 2 - 1) * y' EXP 2 + 1) /\
 364                     (&x + &y * sqrt(&a pow 2 - &1) =
 365                      (&x' + &y' * sqrt(&a pow 2 - &1)) *
 366                      (&a + sqrt(&a pow 2 - &1)))`,
 367   REPEAT STRIP_TAC THEN
 368   EXISTS_TAC `a * x - (a EXP 2 - 1) * y` THEN
 369   EXISTS_TAC `a * y - x:num` THEN
 370   SUBGOAL_THEN `x <= a * y:num` ASSUME_TAC THENL
 371    [ONCE_REWRITE_TAC[GSYM(SPECL [`x:num`; `y:num`; `1`] EXP_MONO_LE_SUC)] THEN
 372     ASM_REWRITE_TAC[ARITH_SUC] THEN
 373     REWRITE_TAC[GSYM ADD1; LE_SUC_LT] THEN
 374     REWRITE_TAC[MULT_EXP; LT_MULT_RCANCEL] THEN
 375     REWRITE_TAC[ARITH_RULE `a - 1 < a <=> ~(a = 0)`] THEN
 376     ASM_REWRITE_TAC[EXP_EQ_0]; ALL_TAC] THEN
 377   SUBGOAL_THEN `(a EXP 2 - 1) * y <= a * x:num` ASSUME_TAC THENL
 378    [SUBGOAL_THEN `(a EXP 2 - 1) * y EXP 2 < a * x * y` MP_TAC THENL
 379      [ALL_TAC;
 380       ASM_SIMP_TAC[MULT_ASSOC; EXP_2; LT_MULT_RCANCEL; LT_IMP_LE]] THEN
 381     REWRITE_TAC[GSYM LE_SUC_LT; ADD1] THEN
 382     FIRST_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [SYM th]) THEN
 383     GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
 384     REWRITE_TAC[EXP_2; GSYM MULT_ASSOC; LE_MULT_LCANCEL] THEN
 385     DISJ2_TAC THEN ONCE_REWRITE_TAC[MULT_SYM] THEN ASM_REWRITE_TAC[];
 386     ALL_TAC] THEN
 387   MATCH_MP_TAC(TAUT `d /\ (d ==> a /\ b /\ c)
 388                      ==> a /\ b /\ c /\ d`) THEN
 389   CONJ_TAC THENL
 390    [MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN
 391     EXISTS_TAC `&a - sqrt(&a pow 2 - &1)` THEN CONJ_TAC THENL
 392      [REWRITE_TAC[REAL_SUB_0] THEN
 393       DISCH_THEN(MP_TAC o C AP_THM `2` o AP_TERM `(pow)`) THEN
 394       ASM_SIMP_TAC[SQRT_POW_2; REAL_SUB_LE; REAL_POW_LE_1; REAL_OF_NUM_LE;
 395                    ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
 396       REAL_ARITH_TAC; ALL_TAC] THEN
 397     REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
 398     REWRITE_TAC[REAL_ARITH `(a + b) * (a - b) = a * a - b * b`] THEN
 399     ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2;  REAL_SUB_LE; REAL_POW_LE_1;
 400                  REAL_OF_NUM_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
 401     REWRITE_TAC[REAL_ARITH `a - (a - b) = b`; REAL_MUL_RID] THEN
 402     ASM_SIMP_TAC[GSYM REAL_OF_NUM_SUB] THEN
 403     REWRITE_TAC[REAL_ARITH
 404      `(x + y * s) * (a - s) = (a * x - (s * s) * y) + (a * y - x) * s`] THEN
 405     ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2;  REAL_SUB_LE; REAL_POW_LE_1;
 406                  REAL_OF_NUM_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
 407     REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
 408     AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
 409     AP_THM_TAC THEN AP_TERM_TAC THEN
 410     REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
 411     REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
 412     ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
 413                  ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
 414   DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
 415   SUBGOAL_THEN
 416    `(&x - &y * sqrt(&a pow 2 - &1)) =
 417     (&(a * x - (a EXP 2 - 1) * y) - &(a * y - x) * sqrt (&a pow 2 - &1)) *
 418     (&a - sqrt(&a pow 2 - &1))`
 419   MP_TAC THENL
 420    [MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN
 421     EXISTS_TAC `&a + sqrt(&a pow 2 - &1)` THEN CONJ_TAC THENL
 422      [MATCH_MP_TAC(REAL_ARITH `~(a = --b) ==> ~(a + b = &0)`) THEN
 423       DISCH_THEN(MP_TAC o C AP_THM `2` o AP_TERM `(pow)`) THEN
 424       REWRITE_TAC[REAL_POW_NEG; ARITH] THEN
 425       ASM_SIMP_TAC[SQRT_POW_2; REAL_SUB_LE; REAL_POW_LE_1; REAL_OF_NUM_LE;
 426                    ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
 427       REAL_ARITH_TAC; ALL_TAC] THEN
 428     REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
 429     REWRITE_TAC[REAL_ARITH `(a - b) * (a + b) = a * a - b * b`] THEN
 430     ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2;  REAL_SUB_LE; REAL_POW_LE_1;
 431                  REAL_OF_NUM_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
 432     REWRITE_TAC[REAL_ARITH `a - (a - b) = b`; REAL_MUL_RID] THEN
 433     ASM_SIMP_TAC[GSYM REAL_OF_NUM_SUB] THEN
 434     REWRITE_TAC[REAL_ARITH
 435      `(x - y * s) * (a + s) = (a * x - (s * s) * y) - (a * y - x) * s`] THEN
 436     ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2;  REAL_SUB_LE; REAL_POW_LE_1;
 437                  REAL_OF_NUM_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
 438     REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
 439     AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
 440     AP_THM_TAC THEN AP_TERM_TAC THEN
 441     REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
 442     REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
 443     ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
 444                  ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
 445   DISCH_THEN(fun th1 -> DISCH_THEN (fun th2 ->
 446    MP_TAC(MK_COMB(AP_TERM `( * )` th1,th2)))) THEN
 447   ONCE_REWRITE_TAC[AC REAL_MUL_AC
 448    `(a * b) * (c * d) = (c * a) * (d * b)`] THEN
 449   REWRITE_TAC[REAL_ARITH `(a + b) * (a - b) = a * a - b * b`] THEN
 450   REWRITE_TAC[REAL_ARITH `(a - b) * (a + b) = a * a - b * b`] THEN
 451   ONCE_REWRITE_TAC[AC REAL_MUL_AC
 452    `(a * b) * (c * b) = (c * a) * (b * b)`] THEN
 453   ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2;  REAL_SUB_LE; REAL_POW_LE_1;
 454                REAL_OF_NUM_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
 455   REWRITE_TAC[REAL_ARITH `a - (a - b) = b`; REAL_MUL_RID] THEN
 456   ASM_REWRITE_TAC[REAL_OF_NUM_POW] THEN
 457   REWRITE_TAC[GSYM REAL_OF_NUM_POW; GSYM REAL_OF_NUM_ADD;
 458               GSYM REAL_OF_NUM_MUL] THEN
 459   SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` (SUBST1_TAC o SYM) THENL
 460    [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
 461     REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
 462     ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
 463                  ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
 464   DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
 465    `((a * b + &1) - b * a = x - y) ==> (x = y + &1)`)) THEN
 466   SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` SUBST1_TAC THENL
 467    [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
 468     REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
 469     ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
 470                  ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
 471   ASM_SIMP_TAC[REAL_OF_NUM_SUB; REAL_OF_NUM_ADD; REAL_OF_NUM_EQ;
 472                REAL_OF_NUM_POW; REAL_OF_NUM_MUL] THEN
 473   ABBREV_TAC `u = a * x - (a EXP 2 - 1) * y` THEN
 474   ABBREV_TAC `v = a * y - x:num` THEN
 475   DISCH_THEN(ASSUME_TAC o ONCE_REWRITE_RULE[MULT_SYM]) THEN
 476   REWRITE_TAC[MULT_AC] THEN
 477   MATCH_MP_TAC(TAUT `(a <=> b) /\ (~a /\ ~b ==> F) ==> a /\ b`) THEN
 478   CONJ_TAC THENL
 479    [GEN_REWRITE_TAC LAND_CONV [GSYM(SPEC `1` EXP_MONO_LT_SUC)] THEN
 480     ASM_REWRITE_TAC[ARITH_SUC] THEN
 481     REWRITE_TAC[LT_ADD_RCANCEL; LT_MULT_LCANCEL] THEN
 482     REWRITE_TAC[num_CONV `2`; EXP_MONO_LT_SUC] THEN
 483     MATCH_MP_TAC(TAUT `a ==> (a /\ b <=> b)`) THEN
 484     REWRITE_TAC[SUB_EQ_0; ARITH_SUC; NOT_LE] THEN
 485     SUBST1_TAC(SYM(SPEC `a:num` (CONJUNCT1 EXP))) THEN
 486     REWRITE_TAC[LT_EXP] THEN REWRITE_TAC[ARITH] THEN
 487     MATCH_MP_TAC(ARITH_RULE `~(a = 0) /\ ~(a = 1) ==> 2 <= a`) THEN
 488     ASM_REWRITE_TAC[]; ALL_TAC] THEN
 489   REWRITE_TAC[NOT_LT] THEN STRIP_TAC THEN
 490   UNDISCH_TAC
 491    `&x + &y * sqrt (&a pow 2 - &1) =
 492     (&u + &v * sqrt (&a pow 2 - &1)) * (&a + sqrt (&a pow 2 - &1))` THEN
 493   REWRITE_TAC[] THEN
 494   MATCH_MP_TAC(REAL_ARITH `a < b ==> ~(a = b)`) THEN
 495   MATCH_MP_TAC REAL_LET_TRANS THEN
 496   EXISTS_TAC `(&u + &v * sqrt (&a pow 2 - &1)) * &1` THEN CONJ_TAC THENL
 497    [REWRITE_TAC[REAL_MUL_RID] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN
 498     ASM_REWRITE_TAC[REAL_OF_NUM_LE] THEN
 499     MATCH_MP_TAC REAL_LE_RMUL THEN
 500     ASM_SIMP_TAC[REAL_OF_NUM_LE; SQRT_POS_LE; REAL_POW_LE_1;
 501                  REAL_SUB_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`];
 502     ALL_TAC] THEN
 503   MATCH_MP_TAC REAL_LT_LMUL THEN CONJ_TAC THENL
 504    [MATCH_MP_TAC REAL_LTE_ADD THEN CONJ_TAC THENL
 505      [REWRITE_TAC[REAL_OF_NUM_LT; LT_NZ] THEN DISCH_THEN SUBST_ALL_TAC THEN
 506       UNDISCH_TAC `0 EXP 2 = (a EXP 2 - 1) * v EXP 2 + 1` THEN
 507       DISCH_THEN(MP_TAC o SYM) THEN CONV_TAC NUM_REDUCE_CONV THEN
 508       REWRITE_TAC[ADD_EQ_0; ARITH_EQ]; ALL_TAC] THEN
 509     MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_POS] THEN
 510     ASM_SIMP_TAC[REAL_OF_NUM_LE; SQRT_POS_LE; REAL_POW_LE_1;
 511                  REAL_SUB_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`];
 512     ALL_TAC] THEN
 513   MATCH_MP_TAC(REAL_ARITH `&1 < x /\ &0 <= y ==> &1 < x + y`) THEN
 514   ASM_SIMP_TAC[REAL_OF_NUM_LE; SQRT_POS_LE; REAL_POW_LE_1;
 515                REAL_SUB_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
 516   REWRITE_TAC[REAL_OF_NUM_LT] THEN
 517   MATCH_MP_TAC(ARITH_RULE `~(a = 0) /\ ~(a = 1) ==> 1 < a`) THEN
 518   ASM_REWRITE_TAC[]);;
 519
 520 let SOLUTIONS_ARE_XY = prove
 521  (`!a x y.
 522     ~(a = 0) /\
 523     (x EXP 2 = (a EXP 2 - 1) * y EXP 2 + 1)
 524     ==> ?n. (x = X a n) /\ (y = Y a n)`,
 525   REPEAT GEN_TAC THEN ASM_CASES_TAC `a = 1` THENL
 526    [ASM_REWRITE_TAC[ARITH; MULT_CLAUSES; ADD_CLAUSES; EXP_2] THEN
 527     SIMP_TAC[MULT_EQ_1; X_DEGENERATE; Y_DEGENERATE; GSYM EXISTS_REFL];
 528     ALL_TAC] THEN
 529   STRIP_TAC THEN
 530   SUBGOAL_THEN `?n. &x + &y * sqrt(&a pow 2 - &1) =
 531                     (&a + sqrt(&a pow 2 - &1)) pow n`
 532   MP_TAC THENL
 533    [UNDISCH_TAC `x EXP 2 = (a EXP 2 - 1) * y EXP 2 + 1` THEN
 534     SPEC_TAC(`x:num`,`x:num`) THEN SPEC_TAC(`y:num`,`y:num`) THEN
 535     MATCH_MP_TAC num_WF THEN X_GEN_TAC `y0:num` THEN DISCH_TAC THEN
 536     X_GEN_TAC `x0:num` THEN
 537     ASM_CASES_TAC `y0 = 0` THENL
 538      [ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES; ADD_CLAUSES; MULT_EQ_1] THEN
 539       DISCH_THEN SUBST1_TAC THEN EXISTS_TAC `0` THEN
 540       REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID; real_pow]; ALL_TAC] THEN
 541     DISCH_TAC THEN
 542     MP_TAC(SPECL [`a:num`; `x0:num`; `y0:num`] SOLUTIONS_INDUCTION) THEN
 543     ASM_REWRITE_TAC[] THEN
 544     DISCH_THEN(X_CHOOSE_THEN `x1:num` (X_CHOOSE_THEN `y1:num`
 545         STRIP_ASSUME_TAC)) THEN
 546     FIRST_X_ASSUM(MP_TAC o SPEC `y1:num`) THEN ASM_REWRITE_TAC[] THEN
 547     DISCH_THEN(MP_TAC o SPEC `x1:num`) THEN ASM_REWRITE_TAC[] THEN
 548     DISCH_THEN(X_CHOOSE_THEN `n:num` SUBST1_TAC) THEN
 549     EXISTS_TAC `SUC n` THEN REWRITE_TAC[real_pow; REAL_MUL_AC]; ALL_TAC] THEN
 550   ASM_SIMP_TAC[GSYM XY_POWER_POS] THEN MATCH_MP_TAC MONO_EXISTS THEN
 551   X_GEN_TAC `n:num` THEN
 552   ASM_SIMP_TAC[SQRT_LINEAR_EQ;
 553                ARITH_RULE `~(a = 0) /\ ~(a = 1) ==> 2 <= a`]);;
 554
 555 (* ------------------------------------------------------------------------- *)
 556 (* Addition formulas.                                                        *)
 557 (* ------------------------------------------------------------------------- *)
 558
 559 let ADDITION_FORMULA_POS = prove
 560  (`!a m n.
 561      ~(a = 0)
 562      ==> ((X a (m + n) = X a m * X a n + (a EXP 2 - 1) * Y a m * Y a n) /\
 563           (Y a (m + n) = X a m * Y a n + X a n * Y a m))`,
 564   REPEAT GEN_TAC THEN DISCH_TAC THEN ASM_CASES_TAC `a = 1` THENL
 565    [ASM_REWRITE_TAC[X_DEGENERATE; Y_DEGENERATE] THEN
 566     REWRITE_TAC[ARITH; MULT_CLAUSES] THEN REWRITE_TAC[ADD_AC]; ALL_TAC] THEN
 567   MP_TAC(SPECL [`a:num`; `m + n:num`] XY_POWER_POS) THEN
 568   MP_TAC(SPECL [`a:num`; `m:num`] XY_POWER_POS) THEN
 569   MP_TAC(SPECL [`a:num`; `n:num`] XY_POWER_POS) THEN
 570   ASM_REWRITE_TAC[] THEN
 571   REWRITE_TAC[REAL_POW_ADD] THEN
 572   DISCH_THEN(SUBST1_TAC o SYM) THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
 573   REWRITE_TAC[REAL_ARITH
 574    `(a + b * s) * (c + d * s) = (a  * c + (s * s) * b * d) +
 575                                 (a * d + b * c) * s`] THEN
 576   ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2;  REAL_SUB_LE; REAL_POW_LE_1;
 577                REAL_OF_NUM_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
 578   SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` SUBST1_TAC THENL
 579    [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
 580     REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
 581     ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
 582                  ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
 583   REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_ADD] THEN
 584   SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` (SUBST1_TAC o SYM) THENL
 585    [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
 586     REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
 587     ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
 588                  ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
 589   ASM_SIMP_TAC[SQRT_LINEAR_EQ;
 590                ARITH_RULE `~(a = 0) /\ ~(a = 1) ==> 2 <= a`] THEN
 591   REWRITE_TAC[MULT_AC]);;
 592
 593 let ADDITION_FORMULA_NEG = prove
 594  (`!a m n.
 595      ~(a = 0) /\ m <= n
 596      ==> ((X a (n - m) = X a m * X a n - (a EXP 2 - 1) * Y a m * Y a n) /\
 597           (Y a (n - m) = X a m * Y a n - X a n * Y a m))`,
 598   REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_CASES_TAC `a = 1` THENL
 599    [ASM_REWRITE_TAC[X_DEGENERATE; Y_DEGENERATE] THEN
 600     REWRITE_TAC[ARITH; MULT_CLAUSES]; ALL_TAC] THEN
 601   MP_TAC(SPECL [`a:num`; `n - m:num`] XY_POWER_POS) THEN
 602   ASM_REWRITE_TAC[] THEN
 603   DISCH_THEN(MP_TAC o AP_TERM
 604    `( * ) (((&a - sqrt (&a pow 2 - &1)) *
 605             (&a + sqrt (&a pow 2 - &1))) pow m)`) THEN
 606   GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)
 607    [REAL_ARITH `(x - y) * (x + y) = x * x - y * y`] THEN
 608   ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2; REAL_SUB_LE;
 609                REAL_POW_LE_1; REAL_OF_NUM_LE;
 610                ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
 611   REWRITE_TAC[REAL_ARITH `x - (x - &1) = &1`] THEN
 612   REWRITE_TAC[REAL_POW_MUL; REAL_POW_ONE; REAL_MUL_LID] THEN
 613   REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
 614   REWRITE_TAC[GSYM REAL_POW_ADD] THEN
 615   ASM_SIMP_TAC[ARITH_RULE `m <= n ==> (m + (n - m) = n:num)`] THEN
 616   MP_TAC(SPECL [`a:num`; `m:num`] XY_POWER_NEG) THEN
 617   MP_TAC(SPECL [`a:num`; `n:num`] XY_POWER_POS) THEN
 618   ASM_REWRITE_TAC[] THEN
 619   DISCH_THEN(SUBST1_TAC o SYM) THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
 620   REWRITE_TAC[REAL_ARITH
 621    `(a - b * s) * (c + d * s) = (a * c - (s * s) * b * d) +
 622                                 (a * d - b * c) * s`] THEN
 623   ASM_SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2;  REAL_SUB_LE; REAL_POW_LE_1;
 624                REAL_OF_NUM_LE; ARITH_RULE `~(a = 0) ==> 1 <= a`] THEN
 625   ONCE_REWRITE_TAC[REAL_ARITH
 626    `(a + b * s = (x1 - x2) + (y1 - y2) * s) =
 627     ((a + x2) + (b + y2) * s = x1 + y1 * s)`] THEN
 628   SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` SUBST1_TAC THENL
 629    [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
 630     REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
 631     ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
 632                  ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
 633   REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_ADD] THEN
 634   SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` (SUBST1_TAC o SYM) THENL
 635    [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
 636     REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
 637     ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
 638                  ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
 639   ASM_SIMP_TAC[SQRT_LINEAR_EQ;
 640                ARITH_RULE `~(a = 0) /\ ~(a = 1) ==> 2 <= a`] THEN
 641   DISCH_THEN(CONJUNCTS_THEN(SUBST1_TAC o SYM)) THEN
 642   REWRITE_TAC[MULT_AC] THEN REWRITE_TAC[ADD_SUB]);;
 643
 644 (* ------------------------------------------------------------------------- *)
 645 (* Some stronger monotonicity theorems for Y.                                *)
 646 (* ------------------------------------------------------------------------- *)
 647
 648 let Y_INCREASES_SUC = prove
 649  (`!a n. ~(a = 0) ==> Y a n < Y a (SUC n)`,
 650   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[ADD1; ADDITION_FORMULA_POS] THEN
 651   REWRITE_TAC[X_CLAUSES; Y_CLAUSES] THEN
 652   MATCH_MP_TAC(ARITH_RULE `1 * y <= ay /\ ~(x = 0) ==> y < x * 1 + ay`) THEN
 653   ASM_SIMP_TAC[LE_MULT_RCANCEL; ARITH_RULE `1 <= a <=> ~(a = 0)`] THEN
 654   MATCH_MP_TAC(ARITH_RULE
 655     `!n. (n = 1) /\ n <= m ==> ~(m = 0)`) THEN
 656   EXISTS_TAC `X a 0` THEN CONJ_TAC THENL
 657    [REWRITE_TAC[X_CLAUSES]; ALL_TAC] THEN
 658   SPEC_TAC(`n:num`,`n:num`) THEN
 659   INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; LE_REFL] THEN
 660   REWRITE_TAC[ADD1] THEN ASM_MESON_TAC[LE_TRANS; X_INCREASES]);;
 661
 662 let Y_INCREASES_LT = prove
 663  (`!a m n. ~(a = 0) /\ m < n ==> Y a m < Y a n`,
 664   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 665   GEN_REWRITE_TAC LAND_CONV [LT_EXISTS] THEN
 666   SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `d:num` THEN DISCH_TAC THEN
 667   MATCH_MP_TAC LTE_TRANS THEN EXISTS_TAC `Y a (SUC m)` THEN
 668   ASM_SIMP_TAC[Y_INCREASES_SUC] THEN
 669   REWRITE_TAC[ARITH_RULE `m + SUC d = SUC m + d`] THEN
 670   SPEC_TAC(`d:num`,`d:num`) THEN
 671   INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; LE_REFL] THEN
 672   RULE_ASSUM_TAC(REWRITE_RULE[ADD_CLAUSES]) THEN
 673   ASM_MESON_TAC[ADD1; LE_TRANS; Y_INCREASES]);;
 674
 675 let Y_INCREASES_LE = prove
 676  (`!a m n. ~(a = 0) /\ m <= n ==> Y a m <= Y a n`,
 677   REWRITE_TAC[LE_LT] THEN MESON_TAC[LE_REFL; Y_INCREASES_LT]);;
 678
 679 let Y_INJ = prove
 680  (`!a m n. ~(a = 0) ==> ((Y a m = Y a n) <=> (m = n))`,
 681   REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN
 682   MP_TAC(SPEC `a:num` Y_INCREASES_LT) THEN ASM_REWRITE_TAC[] THEN
 683   MESON_TAC[LT_CASES; LT_REFL]);;
 684
 685 (* ------------------------------------------------------------------------- *)
 686 (* One for X (to get the same as Y, need a /= 1).                            *)
 687 (* ------------------------------------------------------------------------- *)
 688
 689 let X_INCREASES_LE = prove
 690  (`!a m n. ~(a = 0) /\ m <= n ==> X a m <= X a n`,
 691   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 692   GEN_REWRITE_TAC LAND_CONV [LE_EXISTS] THEN
 693   SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `d:num` THEN
 694   DISCH_THEN(K ALL_TAC) THEN SPEC_TAC(`d:num`,`d:num`) THEN
 695   INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; LE_REFL] THEN
 696   REWRITE_TAC[ADD1] THEN ASM_MESON_TAC[LE_TRANS; X_INCREASES]);;
 697
 698 let X_INCREASES_LT = prove
 699  (`!a m n. ~(a = 0) /\ ~(a = 1) /\ m < n ==> X a m < X a n`,
 700   REPEAT GEN_TAC THEN
 701   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [GSYM LE_SUC_LT] THEN
 702   STRIP_TAC THEN
 703   MATCH_MP_TAC LTE_TRANS THEN EXISTS_TAC `X a (SUC m)` THEN
 704   ASM_SIMP_TAC[X_INCREASES_LE] THEN
 705   SPEC_TAC(`m:num`,`p:num`) THEN
 706   INDUCT_TAC THEN ASM_SIMP_TAC[ARITH; X_CLAUSES; ARITH_RULE
 707    `~(a = 0) /\ ~(a = 1) ==> 1 < a`] THEN
 708   REWRITE_TAC[ARITH_RULE `SUC(SUC p) = p + 2`] THEN
 709   REWRITE_TAC[X_CLAUSES; ADD1] THEN
 710   MATCH_MP_TAC(ARITH_RULE `a <= b /\ c < b ==> a < 2 * b - c`) THEN
 711   CONJ_TAC THENL
 712    [ALL_TAC;
 713     MATCH_MP_TAC LTE_TRANS THEN EXISTS_TAC `X a (SUC p)` THEN
 714     ASM_REWRITE_TAC[]] THEN
 715   GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = 1 * a`] THEN
 716   REWRITE_TAC[LE_MULT_RCANCEL; ADD1] THEN DISJ1_TAC THEN
 717   MAP_EVERY UNDISCH_TAC [`~(a = 0)`; `~(a = 1)`] THEN ARITH_TAC);;
 718
 719 let X_INCREASES_SUC = prove
 720  (`!a n. ~(a = 0) /\ ~(a = 1) ==> X a n < X a (SUC n)`,
 721   SIMP_TAC[X_INCREASES_LT; LT]);;
 722
 723 let X_INJ = prove
 724  (`!a m n. ~(a = 0) /\ ~(a = 1) ==> ((X a m = X a n) <=> (m = n))`,
 725   REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN
 726   MP_TAC(SPEC `a:num` X_INCREASES_LT) THEN ASM_REWRITE_TAC[] THEN
 727   MESON_TAC[LT_CASES; LT_REFL]);;
 728
 729 (* ------------------------------------------------------------------------- *)
 730 (* Coprimality of "X a n" and "Y a n".                                       *)
 731 (* ------------------------------------------------------------------------- *)
 732
 733 let XY_COPRIME = prove
 734  (`!a n. ~(a = 0) ==> coprime(X a n,Y a n)`,
 735   REPEAT GEN_TAC THEN
 736   DISCH_THEN(MP_TAC o SPEC `n:num` o MATCH_MP XY_ARE_SOLUTIONS) THEN
 737   ONCE_REWRITE_TAC[TAUT `a ==> b <=> ~b ==> ~a`] THEN
 738   REWRITE_TAC[coprime; NOT_FORALL_THM; LEFT_IMP_EXISTS_THM] THEN
 739   X_GEN_TAC `d:num` THEN REWRITE_TAC[NOT_IMP] THEN
 740   REWRITE_TAC[divides] THEN STRIP_TAC THEN ASM_REWRITE_TAC[EXP_2] THEN
 741   REWRITE_TAC[GSYM MULT_ASSOC] THEN
 742   GEN_REWRITE_TAC (funpow 2 RAND_CONV o LAND_CONV)
 743    [AC MULT_AC `a * d * x * d * x = d * d * a * x * x:num`] THEN
 744   DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
 745    `(a = b + 1) ==> (a - b = 1)`)) THEN
 746   ASM_REWRITE_TAC[GSYM LEFT_SUB_DISTRIB; MULT_EQ_1]);;
 747
 748 (* ------------------------------------------------------------------------- *)
 749 (* Divisibility properties.                                                  *)
 750 (* ------------------------------------------------------------------------- *)
 751
 752 let Y_DIVIDES_LEMMA = prove
 753  (`!a k n. ~(a = 0) ==> (Y a n) divides (Y a (n * k))`,
 754   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
 755   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN GEN_TAC THEN
 756   INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES] THEN
 757   REWRITE_TAC[Y_CLAUSES; DIVIDES_0] THEN
 758   ASM_SIMP_TAC[ADDITION_FORMULA_POS] THEN
 759   UNDISCH_TAC `Y a n divides Y a (n * k)` THEN
 760   SIMP_TAC[divides; LEFT_IMP_EXISTS_THM] THEN
 761   X_GEN_TAC `d:num` THEN DISCH_TAC THEN
 762   EXISTS_TAC `X a n * d + X a (n * k)` THEN
 763   REWRITE_TAC[LEFT_ADD_DISTRIB] THEN REWRITE_TAC[MULT_AC; ADD_AC]);;
 764
 765 let Y_DIVIDES = prove
 766  (`!a m n. ~(a = 0) ==> ((Y a m) divides (Y a n) <=> m divides n)`,
 767   REPEAT STRIP_TAC THEN EQ_TAC THENL
 768    [ALL_TAC;
 769     GEN_REWRITE_TAC LAND_CONV [divides] THEN
 770     ASM_SIMP_TAC[LEFT_IMP_EXISTS_THM; Y_DIVIDES_LEMMA]] THEN
 771   ONCE_REWRITE_TAC[TAUT `a ==> b <=> ~b ==> ~a`] THEN
 772   ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[DIVIDES_0] THEN
 773   ASM_CASES_TAC `m = 0` THENL
 774    [ASM_REWRITE_TAC[Y_CLAUSES; DIVIDES_ZERO] THEN
 775     MATCH_MP_TAC(ARITH_RULE
 776       `!n. (n = 1) /\ n <= m ==> ~(m = 0)`) THEN
 777     EXISTS_TAC `Y a 1` THEN CONJ_TAC THENL
 778      [REWRITE_TAC[Y_CLAUSES]; ALL_TAC] THEN
 779     ASM_SIMP_TAC[Y_INCREASES_LE; ARITH_RULE `1 <= n <=> ~(n = 0)`];
 780     ALL_TAC] THEN
 781   MP_TAC(SPECL [`n:num`; `m:num`] DIVISION) THEN
 782   ASM_REWRITE_TAC[] THEN
 783   ABBREV_TAC `q = n DIV m` THEN ABBREV_TAC `r = n MOD m` THEN
 784   STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 785   ASM_CASES_TAC `r = 0` THEN
 786   ASM_SIMP_TAC[ADD_CLAUSES; DIVIDES_LMUL; DIVIDES_REFL] THEN
 787   DISCH_TAC THEN
 788   ASM_SIMP_TAC[ADDITION_FORMULA_POS] THEN
 789   SUBGOAL_THEN `~((Y a m) divides (X a (q * m) * Y a r))` MP_TAC THENL
 790    [ALL_TAC;
 791     REWRITE_TAC[TAUT `~a ==> ~b <=> b ==> a`] THEN DISCH_TAC THEN
 792     MATCH_MP_TAC DIVIDES_ADD_REVL THEN
 793     EXISTS_TAC `X a r * Y a (q * m)` THEN
 794     ASM_REWRITE_TAC[] THEN
 795     GEN_REWRITE_TAC (funpow 3 RAND_CONV) [MULT_SYM] THEN
 796     ASM_SIMP_TAC[DIVIDES_LMUL; Y_DIVIDES_LEMMA]] THEN
 797   DISCH_THEN(MP_TAC o MATCH_MP
 798    (REWRITE_RULE[IMP_CONJ] COPRIME_DIVPROD)) THEN
 799   REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
 800    [MP_TAC(SPECL [`a:num`; `q * m:num`] XY_COPRIME) THEN ASM_REWRITE_TAC[] THEN
 801     ONCE_REWRITE_TAC[TAUT `a ==> b <=> ~b ==> ~a`] THEN
 802     REWRITE_TAC[coprime; NOT_FORALL_THM; NOT_IMP] THEN
 803     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:num` THEN
 804     STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
 805     ASM_MESON_TAC[DIVIDES_TRANS; Y_DIVIDES_LEMMA]; ALL_TAC] THEN
 806   DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN
 807   ASM_SIMP_TAC[DE_MORGAN_THM; NOT_LE; Y_INCREASES_LT] THEN
 808   ONCE_REWRITE_TAC[GSYM(CONJUNCT1 Y_CLAUSES)] THEN ASM_SIMP_TAC[Y_INJ]);;
 809
 810 (* ------------------------------------------------------------------------- *)
 811 (* This lemma would be trivial from binomial theorem.                        *)
 812 (* ------------------------------------------------------------------------- *)
 813
 814 let BINOMIAL_TRIVIALITY = prove
 815  (`!x y d n. ?p q.
 816       (&x + &y * sqrt(&d)) pow (n + 2) =
 817       &x pow (n + 2) +
 818       &(n + 2) * &x pow (n + 1) * &y * sqrt(&d) +
 819       &(((n + 1) * (n + 2)) DIV 2) * &x pow n * &y pow 2 * &d +
 820       &p * &y pow 3 + &q * &y pow 3 * sqrt(&d)`,
 821   GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THENL
 822    [REPEAT(EXISTS_TAC `0`) THEN CONV_TAC NUM_REDUCE_CONV THEN
 823     REWRITE_TAC[REAL_POW_1; real_pow; REAL_MUL_LZERO; REAL_ADD_RID] THEN
 824     REWRITE_TAC[REAL_MUL_LID] THEN REWRITE_TAC[REAL_POW_2] THEN
 825     REWRITE_TAC[REAL_ARITH
 826       `(x + y) * (x + y) = x * x + &2 * x * y + y * y`] THEN
 827     AP_TERM_TAC THEN AP_TERM_TAC THEN
 828     ONCE_REWRITE_TAC[AC REAL_MUL_AC `(a * b) * (a * b) = (a * a) * b * b`] THEN
 829     SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2; REAL_POS]; ALL_TAC] THEN
 830   GEN_REWRITE_TAC (funpow 2 BINDER_CONV o LAND_CONV o TOP_DEPTH_CONV)
 831     [ADD_CLAUSES; real_pow] THEN
 832   FIRST_ASSUM(X_CHOOSE_THEN `p:num` (X_CHOOSE_THEN `q:num` SUBST1_TAC)) THEN
 833   REWRITE_TAC[REAL_ARITH
 834    `(x + y) * (xn + xn1 + xn2 + p + q) =
 835     (x * xn) + (x * xn1 + y * xn) + (x * xn2 + y * xn1) +
 836     (y * xn2 + p * x + q * y) + (p * y + q * x)`] THEN
 837   ONCE_REWRITE_TAC[REAL_ARITH
 838    `x * n2 * xn1 * y * d + (y * d) * xn2 = (n2 * x * xn1 + xn2)  * y * d`] THEN
 839   REWRITE_TAC[GSYM(CONJUNCT2 real_pow)] THEN
 840   REWRITE_TAC[ARITH_RULE `SUC(n + m) = n + SUC m`] THEN
 841   REWRITE_TAC[ARITH_RULE `SUC n + m = n + SUC m`] THEN
 842   CONV_TAC NUM_REDUCE_CONV THEN
 843   REWRITE_TAC[REAL_ARITH `&n * x + x = (&n + &1) * x`] THEN
 844   REWRITE_TAC[REAL_OF_NUM_ADD; ARITH_RULE `(n + 2) + 1 = n + 3`] THEN
 845   REWRITE_TAC[GSYM REAL_ADD_ASSOC; GSYM REAL_MUL_ASSOC; REAL_EQ_LADD] THEN
 846   ONCE_REWRITE_TAC[REAL_ARITH
 847    `x * n12 * xn * y2 * d + y * s * n2 * xn1 * y * s + a =
 848     (n12 * (x * xn) * y2 * d + n2 * xn1 * (y * y) * (s * s)) + a`] THEN
 849   REWRITE_TAC[GSYM REAL_POW_2; GSYM(CONJUNCT2 real_pow)] THEN
 850   SIMP_TAC[SQRT_POW_2; REAL_POS] THEN
 851   REWRITE_TAC[ADD1; REAL_MUL_ASSOC; GSYM REAL_ADD_RDISTRIB] THEN
 852   SUBGOAL_THEN `&(((n + 1) * (n + 2)) DIV 2) + &(n + 2) =
 853                 &(((n + 2) * (n + 3)) DIV 2)`
 854   SUBST1_TAC THENL
 855    [REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN
 856     CONV_TAC SYM_CONV THEN MATCH_MP_TAC DIV_UNIQ THEN
 857     EXISTS_TAC `0` THEN REWRITE_TAC[ARITH; ADD_CLAUSES] THEN
 858     REWRITE_TAC[ARITH_RULE `(n + 2) * (n + 3) = n * n + 5 * n + 6`] THEN
 859     REWRITE_TAC[ARITH_RULE
 860      `(x + 5 * n + 6 = (y + n + 2) * 2) <=> (x + 3 * n + 2 = 2 * y)`] THEN
 861     REWRITE_TAC[ARITH_RULE `n * n + 3 * n + 2 = (n + 1) * (n + 2)`] THEN
 862     SUBGOAL_THEN `EVEN((n + 1) * (n + 2))` MP_TAC THENL
 863      [REWRITE_TAC[EVEN_MULT; EVEN_ADD; ARITH_EVEN] THEN
 864       CONV_TAC(EQT_INTRO o TAUT); ALL_TAC] THEN
 865     SIMP_TAC[EVEN_EXISTS; LEFT_IMP_EXISTS_THM] THEN
 866     SIMP_TAC[DIV_MULT; ARITH_EQ]; ALL_TAC] THEN
 867   REWRITE_TAC[REAL_EQ_LADD] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
 868   ONCE_REWRITE_TAC[REAL_ARITH `q * y3 * s * y * s = q * y * y3 * s * s`] THEN
 869   SIMP_TAC[GSYM REAL_POW_2; SQRT_POW_2; REAL_POS] THEN
 870   ONCE_REWRITE_TAC[REAL_ARITH
 871    `y * s * nn * xn * y2 * d = nn * d * xn * (y * y2) * s`] THEN
 872   REWRITE_TAC[GSYM(CONJUNCT2 real_pow)] THEN
 873   EXISTS_TAC `p * x + q * y * d:num` THEN REWRITE_TAC[ARITH_SUC] THEN
 874   EXISTS_TAC `((n + 1) * (n + 2)) DIV 2 * d * x EXP n +
 875               p * y + q * x` THEN
 876   REWRITE_TAC[GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD;
 877               GSYM REAL_OF_NUM_POW] THEN
 878   REWRITE_TAC[REAL_ADD_LDISTRIB; REAL_ADD_RDISTRIB] THEN
 879   REWRITE_TAC[REAL_MUL_AC] THEN REWRITE_TAC[REAL_ADD_AC]);;
 880
 881 (* ------------------------------------------------------------------------- *)
 882 (* A lower bound theorem.                                                    *)
 883 (* ------------------------------------------------------------------------- *)
 884
 885 let Y_LOWERBOUND = prove
 886  (`!a n. (2 * a - 1) EXP n <= Y a (n + 1)`,
 887   GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[EXP; ARITH; Y_CLAUSES] THEN
 888   ASM_CASES_TAC `a = 0` THEN ASM_REWRITE_TAC[ARITH; MULT_CLAUSES; LE_0] THEN
 889   REWRITE_TAC[ARITH_RULE `SUC n + 1 = n + 2`; Y_CLAUSES] THEN
 890   MATCH_MP_TAC LE_TRANS THEN
 891   EXISTS_TAC `(2 * a - 1) * Y a (n + 1)` THEN
 892   ASM_REWRITE_TAC[LE_MULT_LCANCEL] THEN
 893   REWRITE_TAC[RIGHT_SUB_DISTRIB; MULT_CLAUSES; GSYM MULT_ASSOC] THEN
 894   MATCH_MP_TAC(ARITH_RULE `a <= b ==> c - b <= c - a:num`) THEN
 895   ASM_SIMP_TAC[Y_INCREASES]);;
 896
 897 let Y_UPPERBOUND = prove
 898  (`!a n. Y a (n + 1) <= (2 * a) EXP n`,
 899   GEN_TAC THEN INDUCT_TAC THEN
 900   REWRITE_TAC[EXP; ADD_CLAUSES; Y_CLAUSES; LE_REFL] THEN
 901   REWRITE_TAC[ARITH_RULE `SUC(n + 1) = n + 2`; Y_CLAUSES] THEN
 902   MATCH_MP_TAC(ARITH_RULE `a <= b ==> a - c <= b:num`) THEN
 903   ASM_REWRITE_TAC[MULT_ASSOC; LE_MULT_LCANCEL]);;
 904
 905 (* ------------------------------------------------------------------------- *)
 906 (* Now a key congruence.                                                     *)
 907 (* ------------------------------------------------------------------------- *)
 908
 909 let XY_Y3_CONGRUENCE = prove
 910  (`!a n k. ~(a = 0)
 911            ==> ?q. Y a (n * k) =
 912                    k * (X a n) EXP (k - 1) * Y a n + q * (Y a n) EXP 3`,
 913   REPEAT STRIP_TAC THEN ASM_CASES_TAC `k = 0` THENL
 914    [EXISTS_TAC `0` THEN
 915     ASM_REWRITE_TAC[Y_CLAUSES; MULT_CLAUSES; ADD_CLAUSES; SUB_0]; ALL_TAC] THEN
 916   ASM_CASES_TAC `a = 1` THENL
 917    [ASM_REWRITE_TAC[X_DEGENERATE; Y_DEGENERATE; EXP_ONE] THEN
 918     EXISTS_TAC `0` THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
 919     REWRITE_TAC[MULT_AC]; ALL_TAC] THEN
 920   ASM_CASES_TAC `k = 1` THENL
 921    [ASM_REWRITE_TAC[MULT_CLAUSES; SUB_REFL; EXP] THEN
 922     EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES]; ALL_TAC] THEN
 923   MP_TAC(SPECL [`a:num`; `n * k:num`] XY_POWER_POS) THEN ASM_REWRITE_TAC[] THEN
 924   REWRITE_TAC[GSYM REAL_POW_POW] THEN
 925   MP_TAC(SPECL [`a:num`; `n:num`] XY_POWER_POS) THEN ASM_REWRITE_TAC[] THEN
 926   REWRITE_TAC[GSYM REAL_POW_POW] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
 927   SUBGOAL_THEN `2 <= k` MP_TAC THENL
 928    [MAP_EVERY UNDISCH_TAC [`~(k = 0)`; `~(k = 1)`] THEN ARITH_TAC;
 929     ALL_TAC] THEN
 930   GEN_REWRITE_TAC LAND_CONV [LE_EXISTS] THEN
 931   DISCH_THEN(X_CHOOSE_THEN `d:num`
 932     (SUBST1_TAC o ONCE_REWRITE_RULE[ADD_SYM])) THEN
 933   MP_TAC(SPECL [`X a n`; `Y a n`; `a EXP 2 - 1`; `d:num`]
 934                BINOMIAL_TRIVIALITY) THEN
 935   SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` (SUBST1_TAC o SYM) THENL
 936    [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
 937     REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
 938     ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
 939                  ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
 940   DISCH_THEN(X_CHOOSE_THEN `p:num` (X_CHOOSE_THEN `q:num` SUBST1_TAC)) THEN
 941   ONCE_REWRITE_TAC[REAL_ARITH
 942    `x1 + y1 + x2 + x3 + y2 = (x1 + x2 + x3) + (y1 + y2)`] THEN
 943   REWRITE_TAC[REAL_MUL_ASSOC; GSYM REAL_ADD_RDISTRIB] THEN
 944   SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` SUBST1_TAC THENL
 945    [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
 946     REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
 947     ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
 948                  ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
 949   REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_MUL; REAL_OF_NUM_ADD] THEN
 950   SUBGOAL_THEN `&a pow 2 - &1 = &(a EXP 2 - 1)` (SUBST1_TAC o SYM) THENL
 951    [REWRITE_TAC[REAL_OF_NUM_POW] THEN MATCH_MP_TAC REAL_OF_NUM_SUB THEN
 952     REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW] THEN
 953     ASM_SIMP_TAC[REAL_POW_LE_1; REAL_OF_NUM_LE;
 954                  ARITH_RULE `~(a = 0) ==> 1 <= a`]; ALL_TAC] THEN
 955   ASM_SIMP_TAC[SQRT_LINEAR_EQ;
 956                ARITH_RULE `~(p = 0) /\ ~(p = 1) ==> 2 <= p`] THEN
 957   DISCH_THEN(K ALL_TAC) THEN
 958   REWRITE_TAC[ARITH_RULE `(d + 2) - 1 = d + 1`] THEN
 959   EXISTS_TAC `q:num` THEN REWRITE_TAC[GSYM MULT_ASSOC]);;
 960
 961 (* ------------------------------------------------------------------------- *)
 962 (* The other key divisibility result.                                        *)
 963 (* ------------------------------------------------------------------------- *)
 964
 965 let Y2_DIVIDES = prove
 966  (`!a m n. ~(a = 0)
 967            ==> (((Y a m) EXP 2) divides (Y a n) <=> (m * Y a m) divides n)`,
 968   REPEAT STRIP_TAC THEN ASM_CASES_TAC `m = 0` THENL
 969    [ASM_REWRITE_TAC[Y_CLAUSES; MULT_CLAUSES; DIVIDES_ZERO; EXP_2] THEN
 970     GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM(CONJUNCT1 Y_CLAUSES)] THEN
 971     ASM_SIMP_TAC[Y_INJ]; ALL_TAC] THEN
 972   SUBGOAL_THEN `~(Y a m = 0)` ASSUME_TAC THENL
 973    [GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM(CONJUNCT1 Y_CLAUSES)] THEN
 974     ASM_SIMP_TAC[Y_INJ]; ALL_TAC] THEN
 975   MATCH_MP_TAC(TAUT
 976    `!c. (a ==> c) /\ (b ==> c) /\ (c ==> (a <=> b)) ==> (a <=> b)`) THEN
 977   EXISTS_TAC `m divides n` THEN REPEAT CONJ_TAC THENL
 978    [DISCH_TAC THEN
 979     SUBGOAL_THEN `(Y a m) divides (Y a n)` MP_TAC THENL
 980      [ALL_TAC; ASM_SIMP_TAC[Y_DIVIDES]] THEN
 981     UNDISCH_TAC `((Y a m) EXP 2) divides (Y a n)` THEN
 982     REWRITE_TAC[divides; EXP_2; GSYM MULT_ASSOC] THEN MESON_TAC[];
 983     REWRITE_TAC[divides; GSYM MULT_ASSOC] THEN MESON_TAC[];
 984     ALL_TAC] THEN
 985   GEN_REWRITE_TAC LAND_CONV [divides] THEN
 986   DISCH_THEN(X_CHOOSE_THEN `k:num` SUBST1_TAC) THEN
 987   MP_TAC(SPECL [`a:num`; `m:num`; `k:num`] XY_Y3_CONGRUENCE) THEN
 988   ASM_REWRITE_TAC[] THEN
 989   DISCH_THEN(X_CHOOSE_THEN `q:num` SUBST1_TAC) THEN
 990   MATCH_MP_TAC EQ_TRANS THEN
 991   EXISTS_TAC `((Y a m) EXP 2) divides (k * (X a m) EXP (k - 1) * Y a m)` THEN
 992   CONJ_TAC THENL
 993    [REWRITE_TAC[num_CONV `3`; EXP] THEN
 994     MESON_TAC[DIVIDES_ADD; DIVIDES_ADD_REVL; DIVIDES_LMUL; DIVIDES_REFL];
 995     ALL_TAC] THEN
 996   REWRITE_TAC[MULT_ASSOC] THEN
 997   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [MULT_SYM] THEN
 998   REWRITE_TAC[EXP_2; GSYM MULT_ASSOC] THEN
 999   ASM_SIMP_TAC[DIVIDES_LMUL2_EQ] THEN
1000   EQ_TAC THEN SIMP_TAC[DIVIDES_RMUL] THEN
1001   DISCH_TAC THEN MATCH_MP_TAC COPRIME_DIVPROD THEN
1002   EXISTS_TAC `X a m EXP (k - 1)` THEN
1003   ONCE_REWRITE_TAC[MULT_SYM] THEN ASM_REWRITE_TAC[] THEN
1004   MATCH_MP_TAC COPRIME_EXP THEN
1005   ONCE_REWRITE_TAC[COPRIME_SYM] THEN ASM_SIMP_TAC[XY_COPRIME]);;
1006
1007 (* ------------------------------------------------------------------------- *)
1008 (* Some more congruences.                                                    *)
1009 (* ------------------------------------------------------------------------- *)
1010
1011 let Y_N_MOD2 = prove
1012  (`!a n. ~(a = 0) ==> ?q. Y a n = 2 * q + n`,
1013   GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
1014   MATCH_MP_TAC PELL_INDUCTION THEN REWRITE_TAC[Y_CLAUSES] THEN
1015   REPEAT CONJ_TAC THENL
1016    [EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES];
1017     EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES];
1018     ALL_TAC] THEN
1019   REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM;
1020               LEFT_IMP_EXISTS_THM] THEN
1021   MAP_EVERY X_GEN_TAC [`n:num`; `q1:num`; `q2:num`] THEN STRIP_TAC THEN
1022   FIRST_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP Y_INCREASES) THEN
1023   ASM_REWRITE_TAC[] THEN
1024   REWRITE_TAC[ARITH_RULE `2 * q1 + n <= 2 * q2 + n + 1 <=> q1 <= q2`] THEN
1025   DISCH_TAC THEN
1026   EXISTS_TAC `(2 * a * q2 - q1) + (a - 1) * (n + 1)` THEN
1027   MATCH_MP_TAC(ARITH_RULE
1028     `v <= u /\ y <= x /\ (2 * (x + z) + w + v = 2 * y + u)
1029      ==> (u - v = 2 * ((x - y) + z) + w)`) THEN
1030   REPEAT CONJ_TAC THENL
1031    [REWRITE_TAC[LEFT_ADD_DISTRIB] THEN
1032     MATCH_MP_TAC(ARITH_RULE
1033      `x <= u /\ y <= v ==> 2 * x + y <= 2 * u + v + w`) THEN
1034     REWRITE_TAC[MULT_ASSOC] THEN CONJ_TAC THEN
1035     GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `n = 1 * n`] THENL
1036      [MATCH_MP_TAC LE_MULT2 THEN ASM_REWRITE_TAC[];
1037       REWRITE_TAC[LE_MULT_RCANCEL] THEN DISJ1_TAC] THEN
1038     UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC;
1039     REWRITE_TAC[MULT_ASSOC] THEN
1040     GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `n = 1 * n`] THEN
1041     MATCH_MP_TAC LE_MULT2 THEN ASM_REWRITE_TAC[] THEN
1042     UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC;
1043     UNDISCH_TAC `~(a = 0)` THEN SPEC_TAC(`a:num`,`a:num`) THEN
1044     INDUCT_TAC THEN REWRITE_TAC[NOT_SUC] THEN
1045     REWRITE_TAC[ARITH_RULE `SUC a - 1 = a`] THEN
1046     REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
1047     ARITH_TAC]);;
1048
1049 let Y_N_MODA1 = prove
1050  (`!a n. ~(a = 0) ==> ?q. Y a n = q * (a - 1) + n`,
1051   GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
1052   ASM_CASES_TAC `a = 1` THENL
1053    [ASM_REWRITE_TAC[SUB_REFL; Y_DEGENERATE; MULT_CLAUSES; ADD_CLAUSES];
1054     ALL_TAC] THEN
1055   MATCH_MP_TAC PELL_INDUCTION THEN REWRITE_TAC[Y_CLAUSES] THEN
1056   REPEAT CONJ_TAC THENL
1057    [EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES];
1058     EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES];
1059     ALL_TAC] THEN
1060   REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM;
1061               LEFT_IMP_EXISTS_THM] THEN
1062   MAP_EVERY X_GEN_TAC [`n:num`; `q1:num`; `q2:num`] THEN
1063   STRIP_TAC THEN
1064   FIRST_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP Y_INCREASES) THEN
1065   ASM_REWRITE_TAC[] THEN
1066   REWRITE_TAC[ARITH_RULE `q1 + n <= q2 + n + 1 <=> q1 <= q2 + 1`] THEN
1067   ASM_CASES_TAC `q2 = 0` THENL
1068    [ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
1069     REWRITE_TAC[ARITH_RULE `a <= 1 <=> (a = 0) \/ (a = 1)`] THEN
1070     ASM_REWRITE_TAC[MULT_EQ_0; MULT_EQ_1] THEN
1071     ASM_REWRITE_TAC[ARITH_RULE `(a - 1 = 0) <=> (a = 0) \/ (a = 1)`] THEN
1072     SIMP_TAC[ARITH_RULE `(a - 1 = 1) <=> (a = 2)`] THEN
1073     STRIP_TAC THEN ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THENL
1074      [EXISTS_TAC `2 * (n + 1)` THEN
1075       UNDISCH_TAC `~(a = 0)` THEN SPEC_TAC(`a:num`,`b:num`) THEN
1076       INDUCT_TAC THEN REWRITE_TAC[NOT_SUC] THEN
1077       REWRITE_TAC[ARITH_RULE `SUC n - 1 = n`] THEN
1078       REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
1079       MATCH_MP_TAC(ARITH_RULE `(a + c = b) ==> (b - a = c:num)`) THEN
1080       ARITH_TAC;
1081       REWRITE_TAC[MULT_ASSOC; ARITH] THEN
1082       REWRITE_TAC[ARITH_RULE `4 * (n + 1) - (1 + n) = 3 * (n + 1)`] THEN
1083       EXISTS_TAC `2 * n + 1` THEN ARITH_TAC];
1084     ALL_TAC] THEN
1085   DISCH_THEN(fun th ->
1086     EXISTS_TAC `2 * (n + 1) + 2 * a * q2 - q1` THEN MP_TAC th) THEN
1087   UNDISCH_TAC `~(a = 1)` THEN
1088   UNDISCH_TAC `~(a = 0)` THEN SPEC_TAC(`a:num`,`b:num`) THEN
1089   INDUCT_TAC THEN REWRITE_TAC[NOT_SUC] THEN
1090   REWRITE_TAC[ARITH_RULE `(SUC n = 1) <=> (n = 0)`] THEN DISCH_TAC THEN
1091   REWRITE_TAC[ARITH_RULE `SUC n - 1 = n`] THEN DISCH_TAC THEN
1092   REWRITE_TAC[RIGHT_ADD_DISTRIB; RIGHT_SUB_DISTRIB] THEN
1093   MATCH_MP_TAC(ARITH_RULE
1094     `v <= u /\ y <= x /\ (u + y = z + x + w + v)
1095      ==> (u - v = (z + (x - y)) + w:num)`) THEN
1096   REPEAT CONJ_TAC THENL
1097    [GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = 1 * a`] THEN
1098     REWRITE_TAC[MULT_ASSOC] THEN MATCH_MP_TAC LE_MULT2 THEN
1099     ASM_REWRITE_TAC[ARITH_RULE `q1 + n <= q2 + n + 1 <=> q1 <= q2 + 1`] THEN
1100     REWRITE_TAC[MULT_CLAUSES] THEN ARITH_TAC;
1101     MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `q2 * b + 1` THEN
1102     ASM_REWRITE_TAC[] THEN
1103     REWRITE_TAC[ARITH_RULE `a + 1 <= b <=> a < b`] THEN
1104     ASM_SIMP_TAC[LT_MULT_RCANCEL] THEN
1105     GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = 1 * a`] THEN
1106     REWRITE_TAC[MULT_ASSOC] THEN
1107     ASM_SIMP_TAC[LT_MULT_RCANCEL] THEN
1108     REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN ARITH_TAC;
1109     REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN ARITH_TAC]);;
1110
1111 let X_CONGRUENT = prove
1112  (`!a b c n. ~(a = 0) ==> ?q. X (a + b * c) n = X a n + q * c`,
1113   GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
1114   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
1115   ASM_CASES_TAC `b * c = 0` THENL
1116    [GEN_TAC THEN EXISTS_TAC `0` THEN
1117     ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES]; ALL_TAC] THEN
1118   UNDISCH_TAC `~(b * c = 0)` THEN
1119   REWRITE_TAC[MULT_EQ_0; DE_MORGAN_THM] THEN STRIP_TAC THEN
1120   MATCH_MP_TAC PELL_INDUCTION THEN REWRITE_TAC[X_CLAUSES] THEN
1121   REPEAT CONJ_TAC THENL
1122    [EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES];
1123     EXISTS_TAC `b:num` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES];
1124     ALL_TAC] THEN
1125   REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM;
1126               LEFT_IMP_EXISTS_THM] THEN
1127   MAP_EVERY X_GEN_TAC [`n:num`; `q1:num`; `q2:num`] THEN
1128   STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1129   REWRITE_TAC[ARITH_RULE
1130    `2 * (x + y) * (u + v) = 2 * x * u + 2 * u * y + 2 * (x + y) * v`] THEN
1131   EXISTS_TAC `(2 * X a (n + 1) * b + 2 * (a + b * c) * q2) - q1` THEN
1132   MATCH_MP_TAC(ARITH_RULE
1133    `a <= x /\ b <= y + z:num /\ ((x - a) + ((y + z) - b) = u)
1134     ==> ((x + y + z) - (a + b) = u)`) THEN
1135   REWRITE_TAC[RIGHT_SUB_DISTRIB; RIGHT_ADD_DISTRIB; GSYM MULT_ASSOC] THEN
1136   CONJ_TAC THENL
1137    [MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `1 * X a (n + 1)` THEN CONJ_TAC THENL
1138      [ASM_SIMP_TAC[MULT_CLAUSES; X_INCREASES]; ALL_TAC] THEN
1139     REWRITE_TAC[MULT_ASSOC; LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
1140     UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC; ALL_TAC] THEN
1141   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `X (a + b * c) n` THEN CONJ_TAC THENL
1142    [ASM_REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] LE_ADD]; ALL_TAC] THEN
1143   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `X (a + b * c) (n + 1)` THEN
1144   CONJ_TAC THENL [ASM_SIMP_TAC[X_INCREASES; ADD_EQ_0]; ALL_TAC] THEN
1145   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC LE_ADD2 THEN CONJ_TAC THENL
1146    [GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
1147     GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = a * 1`] THEN
1148     REWRITE_TAC[GSYM MULT_ASSOC; LE_MULT_LCANCEL] THEN
1149     ASM_REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`; MULT_EQ_0; ARITH_EQ];
1150     MATCH_MP_TAC(ARITH_RULE `a <= y ==> a <= 2 * (x + y)`) THEN
1151     ONCE_REWRITE_TAC[AC MULT_AC `a * b * c * d = (a * b) * (c * d:num)`] THEN
1152     GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = 1 * a`] THEN
1153     REWRITE_TAC[LE_MULT_RCANCEL] THEN
1154     ASM_REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`; MULT_EQ_0; ARITH_EQ]]);;
1155
1156 let Y_CONGRUENT = prove
1157  (`!a b c n. ~(a = 0) ==> ?q. Y (a + b * c) n = Y a n + q * c`,
1158   GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
1159   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
1160   ASM_CASES_TAC `b * c = 0` THENL
1161    [GEN_TAC THEN EXISTS_TAC `0` THEN
1162     ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES]; ALL_TAC] THEN
1163   UNDISCH_TAC `~(b * c = 0)` THEN
1164   REWRITE_TAC[MULT_EQ_0; DE_MORGAN_THM] THEN STRIP_TAC THEN
1165   MATCH_MP_TAC PELL_INDUCTION THEN REWRITE_TAC[Y_CLAUSES] THEN
1166   REPEAT CONJ_TAC THENL
1167    [EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES];
1168     EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES];
1169     ALL_TAC] THEN
1170   REWRITE_TAC[RIGHT_AND_EXISTS_THM; LEFT_AND_EXISTS_THM;
1171               LEFT_IMP_EXISTS_THM] THEN
1172   MAP_EVERY X_GEN_TAC [`n:num`; `q1:num`; `q2:num`] THEN
1173   STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1174   REWRITE_TAC[ARITH_RULE
1175    `2 * (x + y) * (u + v) = 2 * x * u + 2 * u * y + 2 * (x + y) * v`] THEN
1176   EXISTS_TAC `(2 * Y a (n + 1) * b + 2 * (a + b * c) * q2) - q1` THEN
1177   MATCH_MP_TAC(ARITH_RULE
1178    `a <= x /\ b <= y + z:num /\ ((x - a) + ((y + z) - b) = u)
1179     ==> ((x + y + z) - (a + b) = u)`) THEN
1180   REWRITE_TAC[RIGHT_SUB_DISTRIB; RIGHT_ADD_DISTRIB; GSYM MULT_ASSOC] THEN
1181   CONJ_TAC THENL
1182    [MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `1 * Y a (n + 1)` THEN CONJ_TAC THENL
1183      [ASM_SIMP_TAC[MULT_CLAUSES; Y_INCREASES]; ALL_TAC] THEN
1184     REWRITE_TAC[MULT_ASSOC; LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
1185     UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC; ALL_TAC] THEN
1186   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `Y (a + b * c) n` THEN CONJ_TAC THENL
1187    [ASM_REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] LE_ADD]; ALL_TAC] THEN
1188   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `Y (a + b * c) (n + 1)` THEN
1189   CONJ_TAC THENL [ASM_SIMP_TAC[Y_INCREASES; ADD_EQ_0]; ALL_TAC] THEN
1190   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC LE_ADD2 THEN CONJ_TAC THENL
1191    [GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
1192     GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = a * 1`] THEN
1193     REWRITE_TAC[GSYM MULT_ASSOC; LE_MULT_LCANCEL] THEN
1194     ASM_REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`; MULT_EQ_0; ARITH_EQ];
1195     MATCH_MP_TAC(ARITH_RULE `a <= y ==> a <= 2 * (x + y)`) THEN
1196     ONCE_REWRITE_TAC[AC MULT_AC `a * b * c * d = (a * b) * (c * d:num)`] THEN
1197     GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = 1 * a`] THEN
1198     REWRITE_TAC[LE_MULT_RCANCEL] THEN
1199     ASM_REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`; MULT_EQ_0; ARITH_EQ]]);;
1200
1201 (* ------------------------------------------------------------------------- *)
1202 (* A more important congruence.                                              *)
1203 (* ------------------------------------------------------------------------- *)
1204
1205 let X_CONGRUENT_2NJ_POS = prove
1206  (`!a n j. ~(a = 0) ==> ?q. X a (2 * n + j) + X a j = q * X a n`,
1207   REPEAT STRIP_TAC THEN
1208   MP_TAC(SPECL [`a:num`; `n:num`; `n + j:num`] ADDITION_FORMULA_POS) THEN
1209   ASM_REWRITE_TAC[ARITH_RULE `n + n + j = 2 * n + j`] THEN
1210   DISCH_THEN(SUBST1_TAC o CONJUNCT1) THEN
1211   MP_TAC(SPECL [`a:num`; `n:num`; `j:num`] ADDITION_FORMULA_POS) THEN
1212   ASM_REWRITE_TAC[] THEN DISCH_THEN(SUBST1_TAC o CONJUNCT2) THEN
1213   ONCE_REWRITE_TAC[ARITH_RULE
1214    `(xn * a + d * yn * (xn * yj + xj * yn)) + xj =
1215     xn * (a + d * yn * yj) + xj * (d * yn * yn + 1)`] THEN
1216   ASM_SIMP_TAC[GSYM XY_ARE_SOLUTIONS; GSYM EXP_2] THEN
1217   REWRITE_TAC[EXP_2; ARITH_RULE
1218    `xn * a + xj * xn * xn = (a + xj * xn) * xn:num`] THEN
1219   MESON_TAC[]);;
1220
1221 let X_CONGRUENT_4NJ_POS = prove
1222  (`!a n j. ~(a = 0) ==> ?q. X a (4 * n + j) = q * X a n + X a j`,
1223   REPEAT STRIP_TAC THEN
1224   MP_TAC(SPECL [`a:num`; `n:num`; `2 * n + j`] X_CONGRUENT_2NJ_POS) THEN
1225   ASM_REWRITE_TAC[ARITH_RULE `2 * n + 2 * n + j = 4 * n + j`] THEN
1226   DISCH_THEN(X_CHOOSE_THEN `q1:num` MP_TAC) THEN
1227   DISCH_THEN(MP_TAC o C AP_THM `X a j` o AP_TERM `(+):num->num->num`) THEN
1228   REWRITE_TAC[GSYM ADD_ASSOC] THEN
1229   MP_TAC(SPECL [`a:num`; `n:num`; `j:num`] X_CONGRUENT_2NJ_POS) THEN
1230   ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `q2:num` MP_TAC) THEN
1231   DISCH_THEN SUBST1_TAC THEN
1232   DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1233    `(y + q2 = q1 + x) ==> x <= y ==> (y = (q1 - q2) + x:num)`)) THEN
1234   ASM_SIMP_TAC[X_INCREASES_LE; ARITH_RULE `j <= 4 * n + j`] THEN
1235   DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB] THEN
1236   MESON_TAC[]);;
1237
1238 let X_CONGRUENT_4MNJ_POS = prove
1239  (`!a m n j. ~(a = 0) ==> ?q. X a (4 * m * n + j) = q * X a n + X a j`,
1240   GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
1241   DISCH_TAC THEN INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THENL
1242    [REPEAT GEN_TAC THEN EXISTS_TAC `0` THEN
1243     REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES]; ALL_TAC] THEN
1244   UNDISCH_TAC `!n j. ?q. X a (4 * m * n + j) = q * X a n + X a j` THEN
1245   REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
1246   DISCH_THEN(X_CHOOSE_THEN `q1:num` ASSUME_TAC) THEN
1247   MP_TAC(SPECL [`a:num`; `n:num`; `4 * m * n + j`] X_CONGRUENT_4NJ_POS) THEN
1248   ASM_REWRITE_TAC[ARITH_RULE
1249    `4 * (m * n + n) + j = 4 * n + 4 * m * n + j`] THEN
1250   DISCH_THEN(X_CHOOSE_THEN `q2:num` SUBST1_TAC) THEN
1251   EXISTS_TAC `q2 + q1:num` THEN ARITH_TAC);;
1252
1253 let X_CONGRUENT_2NJ_NEG_LEMMA = prove
1254  (`!a n j. ~(a = 0) /\ j <= n ==> ?q. X a (2 * n - j) + X a j = q * X a n`,
1255   REPEAT STRIP_TAC THEN ASM_CASES_TAC `j = n:num` THENL
1256    [EXISTS_TAC `2` THEN ASM_REWRITE_TAC[MULT_2; ADD_SUB]; ALL_TAC] THEN
1257   MP_TAC(SPECL [`a:num`; `n:num`; `n - j:num`] ADDITION_FORMULA_POS) THEN
1258   ASM_SIMP_TAC[ARITH_RULE `j <= n ==> (n + n - j = 2 * n - j)`] THEN
1259   STRIP_TAC THEN
1260   MP_TAC(SPECL [`a:num`; `j:num`; `n:num`] ADDITION_FORMULA_NEG) THEN
1261   ASM_REWRITE_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1262   EXISTS_TAC `(X a j * X a n - (a EXP 2 - 1) * Y a j * Y a n) +
1263               (X a j * X a n - (a EXP 2 - 1) * Y a j * Y a n)` THEN
1264   REWRITE_TAC[ARITH_RULE
1265    `((xn * a + b) + c = (a + d) * xn) <=> (b + c = xn * d:num)`] THEN
1266   REWRITE_TAC[LEFT_SUB_DISTRIB] THEN
1267   MATCH_MP_TAC(ARITH_RULE
1268    `b <= a /\ e <= d /\ (e + a + c = d + b)
1269     ==> ((a - b) + c = d - e:num)`) THEN
1270   REPEAT CONJ_TAC THENL
1271    [REWRITE_TAC[LE_MULT_LCANCEL] THEN REPEAT DISJ2_TAC THEN
1272     FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
1273      `(c = a - b) ==> 1 <= c ==> b <= a`)) THEN
1274     SUBST1_TAC(SYM(SPEC `a:num` (el 1 (CONJUNCTS Y_CLAUSES)))) THEN
1275     MATCH_MP_TAC Y_INCREASES_LE THEN
1276     ASM_SIMP_TAC[ARITH_RULE `j <= n ==> (1 <= n - j <=> ~(j = n))`];
1277     REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
1278     FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
1279      `(c = a - b) ==> 1 <= c ==> b <= a`)) THEN
1280     SUBST1_TAC(SYM(SPEC `a:num` (CONJUNCT1 X_CLAUSES))) THEN
1281     MATCH_MP_TAC X_INCREASES_LE THEN ASM_REWRITE_TAC[LE_0];
1282     REWRITE_TAC[ARITH_RULE
1283      `xn * a * yj * yn + a * yn * xj * yn + xj =
1284       xj * (a * yn * yn + 1) + a * yn * xn * yj`] THEN
1285     ASM_SIMP_TAC[GSYM XY_ARE_SOLUTIONS; GSYM EXP_2] THEN
1286     REWRITE_TAC[EXP_2; MULT_AC]]);;
1287
1288 let X_CONGRUENT_2NJ_NEG = prove
1289  (`!a n j. ~(a = 0) /\ j <= 2 * n ==> ?q. X a (2 * n - j) + X a j = q * X a n`,
1290   REPEAT STRIP_TAC THEN
1291   ASM_CASES_TAC `j <= n:num` THEN ASM_SIMP_TAC[X_CONGRUENT_2NJ_NEG_LEMMA] THEN
1292   MP_TAC(SPECL [`a:num`; `n:num`; `2 * n - j`] X_CONGRUENT_2NJ_NEG_LEMMA) THEN
1293   ASM_SIMP_TAC[ARITH_RULE `~(j <= n) ==> 2 * n - j <= n`] THEN
1294   ASM_SIMP_TAC[ARITH_RULE `y <= x ==> (x - (x - y) = y:num)`] THEN
1295   SIMP_TAC[ADD_AC]);;
1296
1297 (* ------------------------------------------------------------------------- *)
1298 (* The cute GCD fact given by Smorynski.                                     *)
1299 (* ------------------------------------------------------------------------- *)
1300
1301 let XY_GCD_LEMMA = prove
1302  (`!a m n. ~(a = 0) /\ m < n
1303            ==> (gcd(Y a m,Y a n) = Y a (gcd(m,n)))`,
1304   GEN_TAC THEN ASM_CASES_TAC `a = 0` THEN ASM_REWRITE_TAC[] THEN
1305   ASM_CASES_TAC `a = 1` THEN ASM_REWRITE_TAC[Y_DEGENERATE] THEN
1306   MATCH_MP_TAC num_WF THEN X_GEN_TAC `m:num` THEN DISCH_TAC THEN
1307   X_GEN_TAC `n:num` THEN DISCH_TAC THEN
1308   MP_TAC(SPECL [`n:num`; `m:num`] DIVISION) THEN
1309   ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[Y_CLAUSES; GCD_0] THEN
1310   ABBREV_TAC `q = n DIV m` THEN ABBREV_TAC `r = n MOD m` THEN
1311   DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
1312   FIRST_X_ASSUM(MP_TAC o SPEC `r:num`) THEN ASM_REWRITE_TAC[] THEN
1313   DISCH_THEN(MP_TAC o SPEC `m:num`) THEN ASM_REWRITE_TAC[] THEN
1314   MATCH_MP_TAC EQ_IMP THEN BINOP_TAC THENL
1315    [EXPAND_TAC "n" THEN ASM_SIMP_TAC[ADDITION_FORMULA_POS] THEN
1316     GEN_REWRITE_TAC LAND_CONV [GCD_SYM] THEN MATCH_MP_TAC GCD_EQ THEN
1317     X_GEN_TAC `d:num` THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC(TAUT
1318      `(a ==> (b <=> c)) ==> (a /\ b <=> a /\ c)`) THEN
1319     DISCH_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
1320     EXISTS_TAC `d divides (X a (q * m) * Y a r)` THEN CONJ_TAC THENL
1321      [SUBGOAL_THEN `d divides (Y a (q * m))` MP_TAC THENL
1322        [ASM_MESON_TAC[Y_DIVIDES; DIVIDES_TRANS; DIVIDES_LMUL; DIVIDES_REFL];
1323         ALL_TAC] THEN
1324       MESON_TAC[DIVIDES_ADD; DIVIDES_LMUL; DIVIDES_RMUL; DIVIDES_REFL;
1325                 DIVIDES_ADD_REVL];
1326       ALL_TAC] THEN
1327     EQ_TAC THEN SIMP_TAC[DIVIDES_LMUL] THEN
1328     SUBGOAL_THEN `coprime(d,X a (q * m))`
1329      (fun th -> MESON_TAC[COPRIME_DIVPROD; th]) THEN
1330     SUBGOAL_THEN `d divides (Y a (q * m))` MP_TAC THENL
1331      [ASM_MESON_TAC[Y_DIVIDES; DIVIDES_TRANS; DIVIDES_LMUL; DIVIDES_REFL];
1332       ALL_TAC] THEN
1333     MP_TAC(SPECL [`a:num`; `q * m:num`] XY_COPRIME) THEN ASM_REWRITE_TAC[] THEN
1334     DISCH_TAC THEN DISCH_TAC THEN REWRITE_TAC[coprime] THEN
1335     X_GEN_TAC `e:num` THEN STRIP_TAC THEN
1336     UNDISCH_TAC `coprime (X a (q * m),Y a (q * m))` THEN
1337     REWRITE_TAC[coprime] THEN DISCH_THEN(MP_TAC o SPEC `e:num`) THEN
1338     DISCH_THEN MATCH_MP_TAC THEN ASM_MESON_TAC[DIVIDES_TRANS];
1339     AP_TERM_TAC THEN EXPAND_TAC "n" THEN
1340     GEN_REWRITE_TAC I [GSYM DIVIDES_ANTISYM] THEN
1341     POP_ASSUM_LIST(K ALL_TAC) THEN NUMBER_TAC]);;
1342
1343 let XY_GCD = prove
1344  (`!a m n. ~(a = 0) ==> (gcd(Y a m,Y a n) = Y a (gcd(m,n)))`,
1345   REPEAT STRIP_TAC THEN
1346   REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
1347    (SPECL [`m:num`; `n:num`] LT_CASES)
1348   THENL
1349    [ASM_SIMP_TAC[XY_GCD_LEMMA];
1350     ONCE_REWRITE_TAC[GCD_SYM] THEN ASM_SIMP_TAC[XY_GCD_LEMMA];
1351     ASM_REWRITE_TAC[GCD_REFL]]);;
1352
1353 (* ------------------------------------------------------------------------- *)
1354 (* The "step-down" lemma.                                                    *)
1355 (* ------------------------------------------------------------------------- *)
1356
1357 let STEP_DOWN_LEMMA = prove
1358  (`!a i j n q.
1359         ~(a = 0) /\ ~(a = 1) /\
1360         i <= j /\ j <= 2 * n /\
1361         (X a j = q * X a n + X a i)
1362         ==> (i = j) \/ ((a = 2) /\ (n = 1) /\ (i = 0) /\ (j = 2))`,
1363   REPEAT STRIP_TAC THEN ASM_CASES_TAC `j <= n:num` THENL
1364    [ASM_CASES_TAC `i = j:num` THEN ASM_REWRITE_TAC[] THEN
1365     SUBGOAL_THEN `i < n:num` ASSUME_TAC THENL
1366      [ASM_MESON_TAC[LTE_TRANS; LT_LE]; ALL_TAC] THEN
1367     UNDISCH_TAC `X a j = q * X a n + X a i` THEN
1368     ASM_CASES_TAC `q = 0` THEN
1369     ASM_SIMP_TAC[ADD_CLAUSES; MULT_CLAUSES; X_INJ] THEN
1370     DISCH_TAC THEN
1371     MP_TAC(SPECL [`a:num`; `j:num`; `n:num`] X_INCREASES_LE) THEN
1372     ASM_REWRITE_TAC[] THEN
1373     MATCH_MP_TAC(TAUT `~a ==> a ==> b`) THEN
1374     MATCH_MP_TAC(ARITH_RULE `1 <= b /\ 1 * x <= qx ==> ~(qx + b <= x)`) THEN
1375     SIMP_TAC[LE_MULT_RCANCEL] THEN
1376     ASM_SIMP_TAC[ARITH_RULE `~(x = 0) ==> 1 <= x`] THEN
1377     ONCE_REWRITE_TAC[GSYM(CONJUNCT1 X_CLAUSES)] THEN
1378     ASM_SIMP_TAC[X_INCREASES_LE; LE_0]; ALL_TAC] THEN
1379   ASM_CASES_TAC `n = 0` THENL
1380    [UNDISCH_TAC `i <= j:num` THEN UNDISCH_TAC `j <= 2 * n` THEN
1381     ASM_SIMP_TAC[LE; MULT_CLAUSES]; ALL_TAC] THEN
1382   ASM_CASES_TAC `i <= n:num` THENL
1383    [MP_TAC(SPECL [`a:num`; `n:num`; `j:num`] X_CONGRUENT_2NJ_NEG) THEN
1384     ASM_REWRITE_TAC[] THEN
1385     DISCH_THEN(X_CHOOSE_THEN `q1:num` MP_TAC) THEN
1386     UNDISCH_TAC `X a j = q * X a n + X a i` THEN
1387     ASM_CASES_TAC `q = 0` THEN
1388     ASM_SIMP_TAC[ADD_CLAUSES; MULT_CLAUSES; X_INJ] THEN DISCH_TAC THEN
1389     DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1390      `(a + b + c = d:num) ==> (a + c = d - b)`)) THEN
1391     REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB] THEN
1392     ASM_CASES_TAC `i = n:num` THENL
1393      [ASM_REWRITE_TAC[] THEN
1394       DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1395        `(x + n = q * n) ==> (x = q * n - 1 * n)`)) THEN
1396       MATCH_MP_TAC(TAUT `~a ==> a ==> b`) THEN
1397       REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB] THEN
1398       ASM_CASES_TAC `q1 - q - 1 = 0` THENL
1399        [ASM_REWRITE_TAC[MULT_CLAUSES; ARITH_RULE `~(n = 0) <=> 1 <= n`] THEN
1400         ONCE_REWRITE_TAC[GSYM(CONJUNCT1 X_CLAUSES)] THEN
1401         ASM_SIMP_TAC[X_INCREASES_LE; LE_0]; ALL_TAC] THEN
1402       MATCH_MP_TAC(ARITH_RULE
1403        `j < n /\ 1 * n <= a * n ==> ~(j = a * n)`) THEN
1404       ASM_SIMP_TAC[LE_MULT_RCANCEL; ARITH_RULE `~(x = 0) ==> 1 <= x`] THEN
1405       MATCH_MP_TAC X_INCREASES_LT THEN ASM_REWRITE_TAC[] THEN
1406       UNDISCH_TAC `~(j <= n:num)` THEN
1407       UNDISCH_TAC `~(n = 0)` THEN ARITH_TAC; ALL_TAC] THEN
1408     ASM_CASES_TAC `q1 - q = 0` THENL
1409      [ASM_REWRITE_TAC[MULT_CLAUSES; ADD_EQ_0] THEN
1410       MATCH_MP_TAC(TAUT `~c ==> a /\ c ==> b`) THEN
1411       REWRITE_TAC[ARITH_RULE `~(n = 0) <=> 1 <= n`] THEN
1412       ONCE_REWRITE_TAC[GSYM(CONJUNCT1 X_CLAUSES)] THEN
1413       ASM_SIMP_TAC[X_INCREASES_LE; LE_0]; ALL_TAC] THEN
1414     MATCH_MP_TAC(TAUT `(~b ==> a ==> c) ==> a ==> b \/ c`) THEN
1415     DISCH_TAC THEN DISCH_TAC THEN
1416     ASM_CASES_TAC `n = 1` THENL
1417      [UNDISCH_TAC `j <= 2 * n` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN
1418       UNDISCH_TAC `~(j <= n:num)` THEN ASM_REWRITE_TAC[] THEN
1419       REWRITE_TAC[IMP_IMP] THEN
1420       DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1421        `~(j <= 1) /\ j <= 2 ==> (j = 2)`)) THEN
1422       DISCH_THEN SUBST_ALL_TAC THEN REWRITE_TAC[] THEN
1423       UNDISCH_THEN `n = 1` SUBST_ALL_TAC THEN
1424       SUBGOAL_THEN `i = 0` SUBST_ALL_TAC THENL
1425        [MAP_EVERY UNDISCH_TAC [`i <= 1`; `~(i = 1)`] THEN ARITH_TAC;
1426         ALL_TAC] THEN
1427       UNDISCH_TAC `X a (2 * 1 - 2) + X a 0 = (q1 - q) * X a 1` THEN
1428       REWRITE_TAC[ARITH; X_CLAUSES] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN
1429       MATCH_MP_TAC(ARITH_RULE
1430        `~(a = 0) /\ ~(a = 1) /\ a <= 2 ==> (a = 2)`) THEN
1431       ASM_REWRITE_TAC[] THEN
1432       UNDISCH_THEN `(q1 - q) * a = 2` (SUBST1_TAC o SYM) THEN
1433       GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = 1 * a`] THEN
1434       REWRITE_TAC[LE_MULT_RCANCEL] THEN
1435       ASM_SIMP_TAC[ARITH_RULE `~(q = 0) ==> 1 <= q`]; ALL_TAC] THEN
1436     UNDISCH_TAC `X a (2 * n - j) + X a i = (q1 - q) * X a n` THEN
1437     MATCH_MP_TAC(TAUT `~b ==> b ==> a`) THEN
1438     MATCH_MP_TAC(ARITH_RULE
1439      `s < x /\ x <= q * x ==> ~(s = q * x:num)`) THEN
1440     CONJ_TAC THENL
1441      [ALL_TAC;
1442       GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = 1 * a`] THEN
1443       REWRITE_TAC[LE_MULT_RCANCEL] THEN
1444       ASM_SIMP_TAC[ARITH_RULE `~(q = 0) ==> 1 <= q`]] THEN
1445     MATCH_MP_TAC LET_TRANS THEN
1446     EXISTS_TAC `2 * X a (n - 1)` THEN CONJ_TAC THENL
1447      [MATCH_MP_TAC(ARITH_RULE `a <= c /\ b <= c ==> a + b <= 2 * c`) THEN
1448       CONJ_TAC THEN MATCH_MP_TAC X_INCREASES_LE THEN ASM_REWRITE_TAC[] THENL
1449        [UNDISCH_TAC `~(n = 0)` THEN UNDISCH_TAC `~(j <= n:num)` THEN ARITH_TAC;
1450         UNDISCH_TAC `~(i = n:num)` THEN UNDISCH_TAC `i <= n:num` THEN
1451         ARITH_TAC];
1452       ALL_TAC] THEN
1453     SUBGOAL_THEN `n - 1 = (n - 2) + 1` SUBST1_TAC THENL
1454      [UNDISCH_TAC `~(n = 0)` THEN UNDISCH_TAC `~(n = 1)` THEN ARITH_TAC;
1455       ALL_TAC] THEN
1456     SUBGOAL_THEN `n = (n - 2) + 2`
1457      (fun th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [th])
1458     THENL
1459      [UNDISCH_TAC `~(n = 0)` THEN UNDISCH_TAC `~(n = 1)` THEN ARITH_TAC;
1460       ALL_TAC] THEN
1461     REWRITE_TAC[X_CLAUSES] THEN
1462     MATCH_MP_TAC(ARITH_RULE `z < x /\ 3 * x <= y ==> 2 * x < y - z`) THEN
1463     ASM_SIMP_TAC[X_INCREASES_LT; ARITH_RULE `n < n + 1`] THEN
1464     REWRITE_TAC[MULT_ASSOC; LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
1465     UNDISCH_TAC `~(a = 1)` THEN UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC;
1466     ALL_TAC] THEN
1467   MP_TAC(SPECL [`a:num`; `n:num`; `j:num`] X_CONGRUENT_2NJ_NEG) THEN
1468   ASM_REWRITE_TAC[] THEN
1469   DISCH_THEN(X_CHOOSE_THEN `q1:num` MP_TAC) THEN
1470   MP_TAC(SPECL [`a:num`; `n:num`; `i:num`] X_CONGRUENT_2NJ_NEG) THEN
1471   ANTS_TAC THENL
1472    [ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[LE_TRANS]; ALL_TAC] THEN
1473   DISCH_THEN(X_CHOOSE_THEN `q2:num` MP_TAC) THEN
1474   ASM_REWRITE_TAC[] THEN
1475   REWRITE_TAC[IMP_IMP] THEN
1476   DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1477    `(a = b) /\ (c = d) ==> (a + d = b + c:num)`)) THEN
1478   REWRITE_TAC[ARITH_RULE
1479     `((x + i) + q1 = q2 + y + q3 + i) <=> (x + q1 = y + q2 + q3:num)`] THEN
1480   DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1481    `(x + q1 = y + q2) ==> y <= x ==> (x = y + (q2 - q1:num))`)) THEN
1482   ANTS_TAC THENL
1483    [MATCH_MP_TAC X_INCREASES_LE THEN ASM_REWRITE_TAC[] THEN
1484     UNDISCH_TAC `i <= j:num` THEN ARITH_TAC; ALL_TAC] THEN
1485   REWRITE_TAC[GSYM RIGHT_ADD_DISTRIB; GSYM RIGHT_SUB_DISTRIB] THEN
1486   ASM_CASES_TAC `(q2 + q) - q1 = 0` THENL
1487    [ASM_SIMP_TAC[ADD_CLAUSES; MULT_CLAUSES; X_INJ] THEN
1488     MATCH_MP_TAC(TAUT `(a ==> b) ==> (a ==> b \/ c)`) THEN
1489     UNDISCH_TAC `j <= 2 * n` THEN UNDISCH_TAC `i <= j:num` THEN ARITH_TAC;
1490     ALL_TAC] THEN
1491   MATCH_MP_TAC(TAUT `~a ==> a ==> b`) THEN
1492   MATCH_MP_TAC(ARITH_RULE
1493    `1 * xi <= qxn /\ 1 <= xj ==> ~(xi = xj + qxn)`) THEN
1494   CONJ_TAC THENL
1495    [MATCH_MP_TAC LE_MULT2 THEN
1496     ASM_REWRITE_TAC[ARITH_RULE `1 <= a <=> ~(a = 0)`] THEN
1497     MATCH_MP_TAC X_INCREASES_LE THEN ASM_REWRITE_TAC[] THEN
1498     UNDISCH_TAC `~(i <= n:num)` THEN ARITH_TAC; ALL_TAC] THEN
1499   REWRITE_TAC[GSYM(CONJUNCT1 X_CLAUSES)] THEN
1500   MATCH_MP_TAC X_INCREASES_LE THEN ASM_REWRITE_TAC[LE_0]);;
1501
1502 let STEP_DOWN_LEMMA_4_ASYM = prove
1503  (`!a i j n q.
1504         ~(a = 0) /\ ~(a = 1) /\
1505         0 < i /\ i <= n /\ j < 4 * n /\
1506         (X a i + q * X a n = X a j)
1507         ==> (j = i) \/ (j = 4 * n - i)`,
1508   REPEAT STRIP_TAC THEN ASM_CASES_TAC `j <= 2 * n` THENL
1509    [MP_TAC(SPECL [`a:num`; `i:num`; `j:num`; `n:num`; `q:num`]
1510        STEP_DOWN_LEMMA) THEN
1511     ANTS_TAC THENL
1512      [ASM_REWRITE_TAC[] THEN
1513       UNDISCH_TAC `X a i + q * X a n = X a j` THEN
1514       SIMP_TAC[ADD_AC; MULT_AC] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN
1515       SUBGOAL_THEN `X a i <= X a j` MP_TAC THENL
1516        [ASM_REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] LE_ADD]; ALL_TAC] THEN
1517       ONCE_REWRITE_TAC[TAUT `a ==> b <=> ~b ==> ~a`] THEN
1518       ASM_SIMP_TAC[X_INCREASES_LT; NOT_LE]; ALL_TAC] THEN
1519     ASM_SIMP_TAC[ARITH_RULE `0 < i ==> ~(i = 0)`]; ALL_TAC] THEN
1520   DISJ_CASES_TAC(SPECL [`i:num`; `4 * n - j`] LE_CASES) THEN
1521   (MP_TAC(SPECL [`a:num`; `n:num`; `2 * n - (4 * n - j)`]
1522                 X_CONGRUENT_2NJ_POS) THEN
1523    MP_TAC(SPECL [`a:num`; `n:num`; `4 * n - j`] X_CONGRUENT_2NJ_NEG) THEN
1524    ASM_SIMP_TAC[ARITH_RULE `~(j <= 2 * n) ==> 4 * n - j <= 2 * n`] THEN
1525    ASM_SIMP_TAC[ARITH_RULE
1526      `j < 4 * n /\ ~(j <= 2 * n)
1527       ==> (2 * n + 2 * n - (4 * n - j) = j)`] THEN
1528    DISCH_THEN(X_CHOOSE_THEN `q1:num` ASSUME_TAC) THEN
1529    DISCH_THEN(X_CHOOSE_THEN `q2:num` MP_TAC) THEN
1530    SUBST1_TAC(SYM(ASSUME `X a i + q * X a n = X a j`)) THEN
1531    UNDISCH_TAC
1532     `X a (2 * n - (4 * n - j)) + X a (4 * n - j) = q1 * X a n` THEN
1533    REWRITE_TAC[IMP_IMP] THEN
1534    DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1535      `(a + b = c) /\ (d + a = e) ==> (b + e = c + d:num)`)))
1536   THENL
1537    [DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1538      `(x + q1 = q2 + y + q3)
1539       ==> y <= x ==> (x = ((q2 + q3) - q1) + y:num)`));
1540     DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1541      `(x + q1 = q2 + y + q3)
1542       ==> x <= y ==> (y = (q1 - (q2 + q3)) + x:num)`))] THEN
1543   REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB; GSYM RIGHT_ADD_DISTRIB] THEN
1544   ASM_SIMP_TAC[X_INCREASES_LE] THEN DISCH_TAC THENL
1545    [MP_TAC(SPECL [`a:num`; `i:num`; `4 * n - j`; `n:num`; `(q1 + q) - q2:num`]
1546       STEP_DOWN_LEMMA) THEN
1547     ANTS_TAC THENL
1548      [ASM_REWRITE_TAC[] THEN UNDISCH_TAC `~(j <= 2 * n)` THEN ARITH_TAC;
1549       ALL_TAC] THEN
1550     ASM_SIMP_TAC[ARITH_RULE `0 < i ==> ~(i = 0)`] THEN
1551     DISCH_TAC THEN DISJ2_TAC THEN UNDISCH_TAC `j < 4 * n` THEN ARITH_TAC;
1552     MP_TAC(SPECL [`a:num`; `4 * n - j`; `i:num`; `n:num`; `q2:num - (q1 + q)`]
1553       STEP_DOWN_LEMMA) THEN
1554     ANTS_TAC THENL
1555      [ASM_REWRITE_TAC[] THEN UNDISCH_TAC `i <= n:num` THEN ARITH_TAC;
1556       ALL_TAC] THEN
1557     ASM_REWRITE_TAC[SUB_EQ_0; GSYM NOT_LT] THEN
1558     DISCH_THEN(SUBST1_TAC o SYM) THEN
1559     DISJ2_TAC THEN UNDISCH_TAC `j < 4 * n` THEN ARITH_TAC]);;
1560
1561 let STEP_DOWN_LEMMA_4 = prove
1562  (`!a i j n q1 q2.
1563         ~(a = 0) /\ ~(a = 1) /\
1564         0 < i /\ i <= n /\ j < 4 * n /\
1565         (X a i + q1 * X a n = X a j + q2 * X a n)
1566         ==> (j = i) \/ (j = 4 * n - i)`,
1567   REPEAT STRIP_TAC THEN ASM_CASES_TAC `j < i:num` THENL
1568    [UNDISCH_TAC `X a i + q1 * X a n = X a j + q2 * X a n` THEN
1569     DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1570       `(x + q1 = y + q2) ==> y < x ==> (x = y + (q2 - q1:num))`)) THEN
1571     ASM_SIMP_TAC[X_INCREASES_LT; GSYM RIGHT_SUB_DISTRIB] THEN
1572     ASM_CASES_TAC `q2 - q1 = 0` THENL
1573      [ASM_SIMP_TAC[MULT_CLAUSES; ADD_CLAUSES; X_INJ]; ALL_TAC] THEN
1574     MATCH_MP_TAC(TAUT `~a ==> a ==> b`) THEN
1575     DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1576      `(i = j + q * n) ==> 1 <= j /\ 1 * n <= q * n ==> ~(i <= n)`)) THEN
1577     ASM_SIMP_TAC[X_INCREASES_LE] THEN
1578     ASM_SIMP_TAC[LE_MULT_RCANCEL;
1579                  ARITH_RULE `~(q2 - q1 = 0) ==> 1 <= q2 - q1`] THEN
1580     ONCE_REWRITE_TAC[GSYM(CONJUNCT1 X_CLAUSES)] THEN
1581     ASM_SIMP_TAC[X_INCREASES_LE; LE_0]; ALL_TAC] THEN
1582   MP_TAC(SPECL [`a:num`; `i:num`; `j:num`; `n:num`; `q1 - q2:num`]
1583                STEP_DOWN_LEMMA_4_ASYM) THEN
1584   DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
1585   REWRITE_TAC[RIGHT_SUB_DISTRIB] THEN
1586   MATCH_MP_TAC(ARITH_RULE
1587    `(i + q1 = j + q2) /\ ~(j < i) ==> (i + q1 - q2 = j:num)`) THEN
1588   RULE_ASSUM_TAC(REWRITE_RULE[NOT_LT]) THEN
1589   ASM_SIMP_TAC[NOT_LT; X_INCREASES_LE]);;
1590
1591 let STEP_DOWN_LEMMA_STRONG_ASYM = prove
1592  (`!a i j n c.
1593         ~(a = 0) /\ ~(a = 1) /\
1594         0 < i /\ i <= n /\
1595         (X a i + c * X a n = X a j)
1596         ==> (?q. j = i + 4 * n * q) \/
1597             (?q. j + i = 4 * n * q)`,
1598   REPEAT STRIP_TAC THEN
1599   MP_TAC(SPECL [`j:num`; `4 * n`] DIVISION) THEN
1600   ABBREV_TAC `q = j DIV (4 * n)` THEN ABBREV_TAC `k = j MOD (4 * n)` THEN
1601   ANTS_TAC THENL
1602    [UNDISCH_TAC `0 < i` THEN UNDISCH_TAC `i <= n:num` THEN ARITH_TAC;
1603     ALL_TAC] THEN
1604   DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
1605   MP_TAC(SPECL [`a:num`; `q:num`; `n:num`; `k:num`] X_CONGRUENT_4MNJ_POS) THEN
1606   ASM_REWRITE_TAC[] THEN
1607   DISCH_THEN(X_CHOOSE_THEN `q1:num` MP_TAC) THEN
1608   SUBST1_TAC(ARITH_RULE `4 * q * n + k = q * 4 * n + k`) THEN
1609   ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST_ALL_TAC THEN
1610   ASM_CASES_TAC `k < i:num` THENL
1611    [UNDISCH_TAC `X a i + c * X a n = q1 * X a n + X a k` THEN
1612     DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1613      `(a + q1 = q2 + b) ==> b < a ==> (a = (q2 - q1) + b:num)`)) THEN
1614     ASM_SIMP_TAC[X_INCREASES_LT] THEN REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB] THEN
1615     ASM_CASES_TAC `q1 - c = 0` THENL
1616      [ASM_SIMP_TAC[MULT_CLAUSES; ADD_CLAUSES; X_INJ] THEN
1617       DISCH_TAC THEN DISJ1_TAC THEN EXISTS_TAC `q:num` THEN
1618       FIRST_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [SYM th]) THEN
1619       REWRITE_TAC[ADD_AC; MULT_AC];
1620       MATCH_MP_TAC(TAUT `~a ==> a ==> b`) THEN
1621       MATCH_MP_TAC(ARITH_RULE
1622        `a <= b /\ 1 <= c ==> ~(a = b + c)`) THEN
1623       CONJ_TAC THENL
1624        [GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `n = 1 * n`] THEN
1625         MATCH_MP_TAC LE_MULT2 THEN
1626         ASM_REWRITE_TAC[ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN
1627         ASM_SIMP_TAC[X_INCREASES_LE; LT_IMP_LE];
1628         SUBST1_TAC(SYM(SPEC `a:num` (CONJUNCT1 X_CLAUSES))) THEN
1629         ASM_SIMP_TAC[X_INCREASES_LE; LE_0]]];
1630     MP_TAC(SPECL [`a:num`; `i:num`; `k:num`; `n:num`; `c - q1:num`]
1631                  STEP_DOWN_LEMMA_4_ASYM) THEN
1632     ANTS_TAC THENL
1633      [ASM_REWRITE_TAC[] THEN
1634       UNDISCH_TAC `X a i + c * X a n = q1 * X a n + X a k` THEN
1635       DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1636        `(a + q1 = q2 + b) ==> ~(b < a) ==> (a + (q1 - q2)= b:num)`)) THEN
1637       REWRITE_TAC[GSYM RIGHT_SUB_DISTRIB] THEN
1638       DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[NOT_LT] THEN
1639       MATCH_MP_TAC X_INCREASES_LE THEN ASM_REWRITE_TAC[GSYM NOT_LT];
1640       ALL_TAC] THEN
1641     DISCH_THEN DISJ_CASES_TAC THENL
1642      [DISJ1_TAC THEN EXISTS_TAC `q:num` THEN
1643       UNDISCH_THEN `q * 4 * n + k = j` (SUBST1_TAC o SYM) THEN
1644       ASM_REWRITE_TAC[MULT_AC; ADD_AC];
1645       DISJ2_TAC THEN EXISTS_TAC `q + 1` THEN
1646       UNDISCH_THEN `q * 4 * n + k = j` (SUBST1_TAC o SYM) THEN
1647       REWRITE_TAC[GSYM ADD_ASSOC; LEFT_ADD_DISTRIB; MULT_CLAUSES] THEN
1648       ASM_REWRITE_TAC[] THEN
1649       MATCH_MP_TAC(ARITH_RULE
1650        `(a' = a) /\ i <= b ==> (a + (b - i) + i = a' + b:num)`) THEN
1651       REWRITE_TAC[MULT_AC] THEN
1652       UNDISCH_TAC `i <= n:num` THEN ARITH_TAC]]);;
1653
1654 let STEP_DOWN_LEMMA_STRONG = prove
1655  (`!a i j n c1 c2.
1656         ~(a = 0) /\ ~(a = 1) /\ 0 < i /\ i <= n /\
1657         (X a i + c1 * X a n = X a j + c2 * X a n)
1658         ==> (?q. j = i + 4 * n * q) \/
1659             (?q. j + i = 4 * n * q)`,
1660   REPEAT STRIP_TAC THEN ASM_CASES_TAC `j < i:num` THENL
1661    [UNDISCH_TAC `X a i + c1 * X a n = X a j + c2 * X a n` THEN
1662     DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1663       `(x + q1 = y + q2) ==> y < x ==> (x = y + (q2 - q1:num))`)) THEN
1664     ASM_SIMP_TAC[X_INCREASES_LT; GSYM RIGHT_SUB_DISTRIB] THEN
1665     ASM_CASES_TAC `c2 - c1 = 0` THENL
1666      [ASM_SIMP_TAC[MULT_CLAUSES; ADD_CLAUSES; X_INJ] THEN
1667       DISCH_THEN(K ALL_TAC) THEN DISJ1_TAC THEN
1668       EXISTS_TAC `0` THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES];
1669       ALL_TAC] THEN
1670     MATCH_MP_TAC(TAUT `~a ==> a ==> b`) THEN
1671     DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1672      `(i = j + q * n) ==> 1 <= j /\ 1 * n <= q * n ==> ~(i <= n)`)) THEN
1673     ASM_SIMP_TAC[X_INCREASES_LE] THEN
1674     ASM_SIMP_TAC[LE_MULT_RCANCEL;
1675                  ARITH_RULE `~(q2 - q1 = 0) ==> 1 <= q2 - q1`] THEN
1676     ONCE_REWRITE_TAC[GSYM(CONJUNCT1 X_CLAUSES)] THEN
1677     ASM_SIMP_TAC[X_INCREASES_LE; LE_0]; ALL_TAC] THEN
1678   MP_TAC(SPECL [`a:num`; `i:num`; `j:num`; `n:num`; `c1 - c2:num`]
1679                STEP_DOWN_LEMMA_STRONG_ASYM) THEN
1680   DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
1681   REWRITE_TAC[RIGHT_SUB_DISTRIB] THEN
1682   MATCH_MP_TAC(ARITH_RULE
1683    `(i + q1 = j + q2) /\ ~(j < i) ==> (i + q1 - q2 = j:num)`) THEN
1684   RULE_ASSUM_TAC(REWRITE_RULE[NOT_LT]) THEN
1685   ASM_SIMP_TAC[NOT_LT; X_INCREASES_LE]);;
1686
1687 (* ------------------------------------------------------------------------- *)
1688 (* Diophantine nature of the Y sequence.                                     *)
1689 (* ------------------------------------------------------------------------- *)
1690
1691 let Y_DIOPH = prove
1692  (`~(a = 0) /\ ~(a = 1) /\ ~(y = 0)
1693    ==> ((y = Y a k) <=>
1694         ?x u v r b p q s t c d.
1695                 0 < r /\
1696                 (x EXP 2 = (a EXP 2 - 1) * y EXP 2 + 1) /\
1697                 (u EXP 2 = (a EXP 2 - 1) * v EXP 2 + 1) /\
1698                 (s EXP 2 = (b EXP 2 - 1) * t EXP 2 + 1) /\
1699                 (v = r * y EXP 2) /\
1700                 (b = 1 + 4 * p * y) /\
1701                 (b = a + q * u) /\
1702                 (s = x + c * u) /\
1703                 (t = k + 4 * d * y) /\
1704                 k <= y)`,
1705   REPEAT STRIP_TAC THEN EQ_TAC THENL
1706    [ALL_TAC;
1707     DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
1708     MP_TAC(SPECL [`a:num`; `x:num`; `y:num`] SOLUTIONS_ARE_XY) THEN
1709     ASM_REWRITE_TAC[] THEN
1710     DISCH_THEN(X_CHOOSE_THEN `i:num` (STRIP_ASSUME_TAC o GSYM)) THEN
1711     MP_TAC(SPECL [`a:num`; `u:num`; `v:num`] SOLUTIONS_ARE_XY) THEN
1712     ASM_REWRITE_TAC[] THEN
1713     DISCH_THEN(X_CHOOSE_THEN `n:num` (STRIP_ASSUME_TAC o GSYM)) THEN
1714     SUBGOAL_THEN `~(b = 0)` ASSUME_TAC THENL
1715      [SUBST1_TAC(SYM(ASSUME `1 + 4 * p * y = b`)) THEN
1716       REWRITE_TAC[ADD_EQ_0; ARITH_EQ]; ALL_TAC] THEN
1717     MP_TAC(SPECL [`b:num`; `s:num`; `t:num`] SOLUTIONS_ARE_XY) THEN
1718     ASM_REWRITE_TAC[] THEN
1719     DISCH_THEN(X_CHOOSE_THEN `j:num` (STRIP_ASSUME_TAC o GSYM)) THEN
1720     SUBGOAL_THEN `y <= v:num` ASSUME_TAC THENL
1721      [SUBST1_TAC(SYM(ASSUME `r * y EXP 2 = v`)) THEN REWRITE_TAC[EXP_2] THEN
1722       GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `y = 1 * y`] THEN
1723       REWRITE_TAC[MULT_ASSOC; LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
1724       ASM_REWRITE_TAC[ARITH_RULE `1 <= a <=> ~(a = 0)`; MULT_EQ_0] THEN
1725       ASM_SIMP_TAC[ARITH_RULE `0 < r ==> ~(r = 0)`]; ALL_TAC] THEN
1726     SUBGOAL_THEN `i <= n:num` ASSUME_TAC THENL
1727      [UNDISCH_TAC `y <= v:num` THEN
1728       SUBST1_TAC(SYM(ASSUME `Y a i = y`)) THEN
1729       SUBST1_TAC(SYM(ASSUME `Y a n = v`)) THEN
1730       ONCE_REWRITE_TAC[TAUT `a ==> b <=> ~b ==> ~a`] THEN
1731       ASM_SIMP_TAC[NOT_LE; Y_INCREASES_LT]; ALL_TAC] THEN
1732     MP_TAC(SPECL [`a:num`; `q:num`; `u:num`; `j:num`] X_CONGRUENT) THEN
1733     REWRITE_TAC[ASSUME `~(a = 0)`; ASSUME `a + q * u = b:num`] THEN
1734     DISCH_THEN(X_CHOOSE_THEN `q1:num` MP_TAC) THEN
1735     SUBST1_TAC(ASSUME `X b j = s`) THEN
1736     SUBST1_TAC(SYM(ASSUME `x + c * u = s:num`)) THEN
1737     SUBST1_TAC(SYM(ASSUME `X a i = x`)) THEN
1738     SUBST1_TAC(SYM(ASSUME `X a n = u`)) THEN DISCH_TAC THEN
1739     SUBGOAL_THEN `~(i = 0)` ASSUME_TAC THENL
1740      [UNDISCH_TAC `~(y = 0)` THEN
1741       REWRITE_TAC[TAUT `~a ==> ~b <=> b ==> a`] THEN
1742       EXPAND_TAC "y" THEN SIMP_TAC[Y_CLAUSES; ASSUME `~(a = 0)`];
1743       ALL_TAC] THEN
1744     SUBGOAL_THEN `(?q. j = i + 4 * n * q) \/ (?q. j + i = 4 * n * q)`
1745     ASSUME_TAC THENL
1746      [MATCH_MP_TAC STEP_DOWN_LEMMA_STRONG THEN
1747       MAP_EVERY EXISTS_TAC [`a:num`; `c:num`; `q1:num`] THEN
1748       ASM_SIMP_TAC[ARITH_RULE `~(i = 0) ==> 0 < i`]; ALL_TAC] THEN
1749     MP_TAC(SPECL [`a:num`; `i:num`; `n:num`] Y2_DIVIDES) THEN
1750     ASM_REWRITE_TAC[] THEN
1751     DISCH_THEN(MP_TAC o fst o EQ_IMP_RULE) THEN
1752     REWRITE_TAC[divides; LEFT_IMP_EXISTS_THM] THEN
1753     DISCH_THEN(MP_TAC o SPEC `r:num`) THEN
1754     SUBST1_TAC(SYM(ASSUME `r * y EXP 2 = v`)) THEN
1755     REWRITE_TAC[EQT_INTRO(SPEC_ALL MULT_SYM)] THEN
1756     DISCH_THEN(X_CHOOSE_THEN `d1:num` (ASSUME_TAC o SYM)) THEN
1757     UNDISCH_TAC `(?q. j = i + 4 * n * q) \/ (?q. j + i = 4 * n * q:num)` THEN
1758     UNDISCH_THEN `(i * y) * d1 = n:num` (SUBST1_TAC o SYM) THEN DISCH_TAC THEN
1759     SUBGOAL_THEN `(?q. j = i + q * 4 * Y a i) \/
1760                   (?q. j + i = q * 4 * Y a i)`
1761     MP_TAC THENL
1762      [FIRST_ASSUM(UNDISCH_TAC o check is_disj o concl) THEN
1763       REWRITE_TAC[OR_EXISTS_THM] THEN
1764       DISCH_THEN(X_CHOOSE_THEN `d2:num`
1765        (fun th -> EXISTS_TAC `i * d1 * d2:num` THEN MP_TAC th)) THEN
1766       SUBST1_TAC(ASSUME `Y a i = y`) THEN REWRITE_TAC[MULT_AC];
1767       FIRST_X_ASSUM(K ALL_TAC o check (is_disj o concl)) THEN
1768       DISCH_TAC] THEN
1769     MP_TAC(SPECL [`b:num`; `j:num`] Y_N_MODA1) THEN
1770     ASM_REWRITE_TAC[] THEN
1771     DISCH_THEN(X_CHOOSE_THEN `d3:num` MP_TAC) THEN
1772     SUBST1_TAC(SYM(ASSUME `1 + 4 * p * y = b`)) THEN REWRITE_TAC[ADD_SUB2] THEN
1773     SUBST1_TAC(SYM(ASSUME `k + 4 * d * y = t`)) THEN DISCH_TAC THEN
1774     SUBST1_TAC(SYM(ASSUME `Y a i = y`)) THEN AP_TERM_TAC THEN
1775     SUBGOAL_THEN `(?q1 q2. k + q1 * 4 * Y a i = i + q2 * 4 * Y a i) \/
1776                   (?q. i + k = q * 4 * Y a i)`
1777     MP_TAC THENL
1778      [UNDISCH_TAC `(?q. j = i + q * 4 * Y a i) \/
1779                    (?q. j + i = q * 4 * Y a i)` THEN
1780       MATCH_MP_TAC(TAUT
1781        `(a1 ==> b1) /\ (a2 ==> b2) ==> a1 \/ a2 ==> b1 \/ b2`) THEN
1782       CONJ_TAC THEN DISCH_TAC THEN
1783       UNDISCH_TAC `k + 4 * d * y = d3 * 4 * p * y + j` THENL
1784        [FIRST_X_ASSUM(X_CHOOSE_THEN `d4:num` SUBST1_TAC) THEN
1785         DISCH_THEN(fun th ->
1786           EXISTS_TAC `d:num` THEN
1787           EXISTS_TAC `d3 * p + d4:num` THEN MP_TAC th) THEN
1788         SUBST1_TAC(SYM(ASSUME `Y a i = y`)) THEN
1789         REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
1790         REWRITE_TAC[MULT_AC] THEN REWRITE_TAC[ADD_AC];
1791         DISCH_THEN(MP_TAC o C AP_THM `i:num` o
1792           AP_TERM `(+):num->num->num`) THEN
1793         REWRITE_TAC[GSYM ADD_ASSOC] THEN
1794         FIRST_X_ASSUM(X_CHOOSE_THEN `d4:num` SUBST1_TAC) THEN
1795         DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1796          `(k + q1 + i = q2) ==> (i + k = q2 - q1:num)`)) THEN
1797         DISCH_THEN SUBST1_TAC THEN
1798         SUBST1_TAC(SYM(ASSUME `Y a i = y`)) THEN
1799         REWRITE_TAC[GSYM RIGHT_ADD_DISTRIB; MULT_ASSOC;
1800                     GSYM RIGHT_SUB_DISTRIB] THEN
1801         REWRITE_TAC[GSYM MULT_ASSOC] THEN
1802         REWRITE_TAC[ARITH_RULE
1803          `(d3 * 4 * p + d4 * 4) - 4 * x =
1804           ((d3 * p + d4) - x) * 4`] THEN REWRITE_TAC[GSYM MULT_ASSOC] THEN
1805         EXISTS_TAC `(d3 * p + d4) - d:num` THEN REFL_TAC];
1806       ALL_TAC] THEN
1807     SUBGOAL_THEN `k <= Y a i` ASSUME_TAC THENL
1808      [ASM_REWRITE_TAC[]; ALL_TAC] THEN
1809     SUBGOAL_THEN `i <= Y a i` ASSUME_TAC THENL
1810      [MP_TAC(SPECL [`a:num`; `i:num`] Y_N_MODA1) THEN
1811       ASM_SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN
1812       REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] LE_ADD]; ALL_TAC] THEN
1813     DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
1814      [DISCH_THEN(X_CHOOSE_THEN `q4:num` (X_CHOOSE_THEN `q5:num` MP_TAC)) THEN
1815       REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
1816        (SPECL [`q4:num`; `q5:num`] LT_CASES)
1817       THENL
1818        [DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1819          `(k + q4 = i + q5) ==> q4 < q5:num ==> (k = i + (q5 - q4))`)) THEN
1820         REWRITE_TAC[MULT_ASSOC; LT_MULT_RCANCEL; GSYM RIGHT_SUB_DISTRIB] THEN
1821         ASM_REWRITE_TAC[MULT_EQ_0; ARITH_EQ] THEN
1822         UNDISCH_TAC `k <= y:num` THEN
1823         MATCH_MP_TAC(TAUT `(a ==> ~b) ==> b ==> a ==> c`) THEN
1824         DISCH_THEN SUBST1_TAC THEN
1825         MATCH_MP_TAC(ARITH_RULE `1 * y < k * y ==> ~(i + k * y <= y)`) THEN
1826         ASM_REWRITE_TAC[LT_MULT_RCANCEL] THEN
1827         UNDISCH_TAC `q4 < q5:num` THEN ARITH_TAC;
1828         DISCH_THEN(MP_TAC o MATCH_MP (ARITH_RULE
1829          `(k + q4 = i + q5) ==> q5 < q4:num ==> (i = k + (q4 - q5))`)) THEN
1830         REWRITE_TAC[MULT_ASSOC; LT_MULT_RCANCEL; GSYM RIGHT_SUB_DISTRIB] THEN
1831         ASM_REWRITE_TAC[MULT_EQ_0; ARITH_EQ] THEN
1832         UNDISCH_TAC `i <= Y a i` THEN
1833         MATCH_MP_TAC(TAUT `(a ==> ~b) ==> b ==> a ==> c`) THEN
1834         ASM_REWRITE_TAC[] THEN
1835         DISCH_THEN SUBST1_TAC THEN
1836         MATCH_MP_TAC(ARITH_RULE `1 * y < k * y ==> ~(i + k * y <= y)`) THEN
1837         ASM_REWRITE_TAC[LT_MULT_RCANCEL] THEN
1838         UNDISCH_TAC `q5 < q4:num` THEN ARITH_TAC;
1839         ASM_SIMP_TAC[EQ_ADD_RCANCEL]];
1840       DISCH_THEN(X_CHOOSE_THEN `q6:num` MP_TAC) THEN
1841       ASM_CASES_TAC `q6 = 0` THEN ASM_REWRITE_TAC[MULT_CLAUSES; ADD_EQ_0] THEN
1842       UNDISCH_TAC `k <= Y a i` THEN UNDISCH_TAC `i <= Y a i` THEN
1843       SUBST1_TAC(ASSUME `Y a i = y`) THEN
1844       MATCH_MP_TAC(ARITH_RULE
1845        `2 * y < ay ==> i <= y ==> k <= y ==> (i + k = ay) ==> (i = k)`) THEN
1846       REWRITE_TAC[MULT_ASSOC; LT_MULT_RCANCEL] THEN ASM_REWRITE_TAC[] THEN
1847       UNDISCH_TAC `~(q6 = 0)` THEN ARITH_TAC]] THEN
1848   DISCH_THEN(ASSUME_TAC o SYM) THEN ABBREV_TAC `x = X a k` THEN
1849   SUBGOAL_THEN `x EXP 2 = (a EXP 2 - 1) * y EXP 2 + 1` (ASSUME_TAC o SYM) THENL
1850    [MAP_EVERY EXPAND_TAC ["x"; "y"] THEN
1851     SIMP_TAC[XY_ARE_SOLUTIONS; ASSUME `~(a = 0)`]; ALL_TAC] THEN
1852   EXISTS_TAC `x:num` THEN ASM_REWRITE_TAC[] THEN
1853   ABBREV_TAC `m = 2 * k * Y a k` THEN
1854   ABBREV_TAC `u = X a m` THEN ABBREV_TAC `v = Y a m` THEN
1855   SUBGOAL_THEN `u EXP 2 = (a EXP 2 - 1) * v EXP 2 + 1` (ASSUME_TAC o SYM) THENL
1856    [MAP_EVERY EXPAND_TAC ["u"; "v"] THEN
1857     SIMP_TAC[XY_ARE_SOLUTIONS; ASSUME `~(a = 0)`]; ALL_TAC] THEN
1858   EXISTS_TAC `u:num` THEN EXISTS_TAC `v:num` THEN ASM_REWRITE_TAC[] THEN
1859   SUBGOAL_THEN `(y EXP 2) divides v` MP_TAC THENL
1860    [SUBST1_TAC(SYM(ASSUME `Y a m = v`)) THEN
1861     SUBST1_TAC(SYM(ASSUME `Y a k = y`)) THEN
1862     SIMP_TAC[Y2_DIVIDES; ASSUME `~(a = 0)`] THEN
1863     SUBST1_TAC(SYM(ASSUME `2 * k * Y a k = m`)) THEN
1864     REWRITE_TAC[divides] THEN EXISTS_TAC `2` THEN
1865     REWRITE_TAC[MULT_AC]; ALL_TAC] THEN
1866   REWRITE_TAC[divides] THEN
1867   DISCH_THEN(X_CHOOSE_THEN `r:num` (ASSUME_TAC o SYM)) THEN
1868   EXISTS_TAC `r:num` THEN ASM_REWRITE_TAC[] THEN
1869   ASM_CASES_TAC `r = 0` THENL
1870    [UNDISCH_TAC `y EXP 2 * r = v` THEN ASM_REWRITE_TAC[MULT_CLAUSES] THEN
1871     DISCH_THEN(ASSUME_TAC o SYM) THEN REWRITE_TAC[LT_REFL] THEN
1872     UNDISCH_TAC `Y a m = v` THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1873     SUBGOAL_THEN `m = 0` ASSUME_TAC THENL
1874      [UNDISCH_TAC `Y a m = 0` THEN
1875       ONCE_REWRITE_TAC[GSYM(CONJUNCT1 Y_CLAUSES)] THEN
1876       SIMP_TAC[Y_INJ; ASSUME `~(a = 0)`] THEN
1877       REWRITE_TAC[Y_CLAUSES]; ALL_TAC] THEN
1878     SUBGOAL_THEN `k = 0` ASSUME_TAC THENL
1879      [UNDISCH_TAC `2 * k * Y a k = m` THEN
1880       REWRITE_TAC[ASSUME `m = 0`; MULT_EQ_0; ARITH_EQ] THEN
1881       ONCE_REWRITE_TAC[GSYM(CONJUNCT1 Y_CLAUSES)] THEN
1882       SIMP_TAC[Y_INJ; ASSUME `~(a = 0)`] THEN
1883       REWRITE_TAC[Y_CLAUSES; EQ_SYM]; ALL_TAC] THEN
1884     UNDISCH_TAC `Y a k = y` THEN ASM_REWRITE_TAC[Y_CLAUSES];
1885     ALL_TAC] THEN
1886   ASM_SIMP_TAC[ARITH_RULE `~(r = 0) ==> 0 < r`] THEN
1887   SUBGOAL_THEN `ODD(u)` ASSUME_TAC THENL
1888    [UNDISCH_TAC `(a EXP 2 - 1) * v EXP 2 + 1 = u EXP 2` THEN
1889     DISCH_THEN(MP_TAC o AP_TERM `EVEN`) THEN
1890     REWRITE_TAC[EXP_2; EVEN_ADD; EVEN_MULT; ARITH_EVEN] THEN
1891     SUBGOAL_THEN `EVEN v` (fun th -> REWRITE_TAC[GSYM NOT_EVEN; th]) THEN
1892     SUBST1_TAC(SYM(ASSUME `Y a m = v`)) THEN
1893     MP_TAC(SPECL [`a:num`; `m:num`] Y_N_MOD2) THEN
1894     SIMP_TAC[ASSUME `~(a = 0)`; LEFT_IMP_EXISTS_THM] THEN
1895     SUBST1_TAC(SYM(ASSUME `2 * k * Y a k = m`)) THEN
1896     REWRITE_TAC[EVEN_ADD; EVEN_MULT; ARITH_EVEN]; ALL_TAC] THEN
1897   SUBGOAL_THEN `?b0 q6 q7. (b0 = 1 + q6 * 4 * y) /\ (b0 = a + q7 * u)`
1898   MP_TAC THENL
1899    [MATCH_MP_TAC CHINESE_REMAINDER THEN
1900     UNDISCH_TAC `ODD u` THEN
1901     ASM_CASES_TAC `u = 0` THEN ASM_REWRITE_TAC[ARITH_ODD] THEN
1902     DISCH_TAC THEN ASM_REWRITE_TAC[MULT_EQ_0; ARITH_EQ] THEN
1903     ONCE_REWRITE_TAC[COPRIME_SYM] THEN MATCH_MP_TAC COPRIME_MUL THEN
1904     CONJ_TAC THENL
1905      [SUBST1_TAC(SYM(NUM_REDUCE_CONV `2 * 2`)) THEN
1906       MATCH_MP_TAC COPRIME_MUL THEN REWRITE_TAC[] THEN
1907       MP_TAC(SPECL [`u:num`; `2`] PRIME_COPRIME) THEN REWRITE_TAC[PRIME_2] THEN
1908       MATCH_MP_TAC(TAUT `~b /\ (a ==> d) /\ (c ==> d)
1909                          ==> a \/ b \/ c ==> d`) THEN
1910       REPEAT CONJ_TAC THENL
1911        [UNDISCH_TAC `ODD u` THEN
1912         ONCE_REWRITE_TAC[TAUT `a ==> b <=> ~b ==> ~a`] THEN
1913         SIMP_TAC[divides; LEFT_IMP_EXISTS_THM; ODD_MULT; ARITH_ODD];
1914         ONCE_REWRITE_TAC[COPRIME_SYM] THEN SIMP_TAC[COPRIME_1];
1915         REWRITE_TAC[COPRIME_SYM]];
1916       MP_TAC(SPECL [`a:num`; `m:num`] XY_COPRIME) THEN ASM_REWRITE_TAC[] THEN
1917       SUBST1_TAC(SYM(ASSUME `y EXP 2 * r = v`)) THEN
1918       REWRITE_TAC[coprime; EXP_2] THEN
1919       MESON_TAC[DIVIDES_RMUL; DIVIDES_LMUL]]; ALL_TAC] THEN
1920   DISCH_THEN(X_CHOOSE_THEN `b:num` (X_CHOOSE_THEN `p:num`
1921         (X_CHOOSE_THEN `q:num` (STRIP_ASSUME_TAC o GSYM)))) THEN
1922   MAP_EVERY EXISTS_TAC [`b:num`; `p:num`; `q:num`] THEN
1923   ONCE_REWRITE_TAC[ARITH_RULE `1 + 4 * p * y = 1 + p * 4 * y`] THEN
1924   ASM_REWRITE_TAC[] THEN
1925   ABBREV_TAC `s = X b k` THEN ABBREV_TAC `t = Y b k` THEN
1926   EXISTS_TAC `s:num` THEN EXISTS_TAC `t:num` THEN
1927   SUBST1_TAC(ARITH_RULE `r * y EXP 2 = y EXP 2 * r`) THEN
1928   ASM_REWRITE_TAC[] THEN
1929   SUBST1_TAC(SYM(ASSUME `X b k = s`)) THEN
1930   SUBST1_TAC(SYM(ASSUME `Y b k = t`)) THEN
1931   SUBGOAL_THEN `~(b = 0)` ASSUME_TAC THENL
1932    [UNDISCH_THEN `1 + p * 4 * y = b` (SUBST1_TAC o SYM) THEN
1933     ONCE_REWRITE_TAC[TAUT `~b ==> a ==> b ==> ~a`] THEN
1934     REWRITE_TAC[ADD_EQ_0; ARITH_EQ]; ALL_TAC] THEN
1935   SIMP_TAC[XY_ARE_SOLUTIONS; ASSUME `~(b = 0)`] THEN
1936   MP_TAC(SPECL [`a:num`; `q:num`; `u:num`; `k:num`] X_CONGRUENT) THEN
1937   ASM_REWRITE_TAC[] THEN
1938   DISCH_THEN(X_CHOOSE_THEN `c:num` (ASSUME_TAC o SYM)) THEN
1939   EXISTS_TAC `c:num` THEN ASM_REWRITE_TAC[] THEN
1940   MP_TAC(SPECL [`b:num`; `k:num`] Y_N_MODA1) THEN
1941   SUBST1_TAC(SYM(ASSUME `1 + p * 4 * y = b`)) THEN
1942   REWRITE_TAC[ADD_EQ_0; ADD_SUB2; ARITH_EQ] THEN ASM_REWRITE_TAC[] THEN
1943   DISCH_THEN(X_CHOOSE_THEN `q8:num` SUBST1_TAC) THEN
1944   EXISTS_TAC `q8 * p:num` THEN REWRITE_TAC[MULT_AC; ADD_AC] THEN
1945   MP_TAC(SPECL [`a:num`; `k:num`] Y_N_MODA1) THEN
1946   ASM_SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN
1947   REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] LE_ADD]);;
1948
1949 (* ------------------------------------------------------------------------- *)
1950 (* A ratio approaches a^n for large enough k.                                *)
1951 (* ------------------------------------------------------------------------- *)
1952
1953 let BINOMIALISH_LEMMA = prove
1954  (`!m n. m EXP n * (m - n) <= m * (m - 1) EXP n`,
1955   GEN_TAC THEN INDUCT_TAC THEN
1956   REWRITE_TAC[EXP; SUB_0; MULT_CLAUSES; LE_REFL] THEN
1957   MATCH_MP_TAC LE_TRANS THEN
1958   EXISTS_TAC `(m - 1) * m EXP n * (m - n)` THEN CONJ_TAC THENL
1959    [REWRITE_TAC[GSYM MULT_ASSOC] THEN
1960     ONCE_REWRITE_TAC[AC MULT_AC `a * b * c = b * a * c:num`] THEN
1961     REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
1962     REWRITE_TAC[LEFT_SUB_DISTRIB; RIGHT_SUB_DISTRIB; MULT_CLAUSES] THEN
1963     ONCE_REWRITE_TAC[ARITH_RULE `a - (b + c) = a - c - b:num`] THEN
1964     MATCH_MP_TAC(ARITH_RULE `c <= b ==> a - b <= a - c:num`) THEN ARITH_TAC;
1965     GEN_REWRITE_TAC RAND_CONV
1966      [AC MULT_AC `m * (m - 1) * n = (m - 1) * m * n`] THEN
1967     ASM_REWRITE_TAC[LE_MULT_LCANCEL]]);;
1968
1969 let XY_EXP_LEMMA = prove
1970  (`!a k n.
1971         ~(a = 0) /\
1972         2 * n * a EXP n < k
1973         ==> abs(&(Y (a * k) (n + 1)) / &(Y k (n + 1)) - &a pow n) < &1 / &2`,
1974   REPEAT STRIP_TAC THEN
1975   SUBGOAL_THEN `~(k = 0)` ASSUME_TAC THENL
1976    [FIRST_ASSUM(ACCEPT_TAC o MATCH_MP (ARITH_RULE
1977      `a < k ==> ~(k = 0)`)); ALL_TAC] THEN
1978   SUBGOAL_THEN `0 < Y k (n + 1)` ASSUME_TAC THENL
1979    [SUBST1_TAC(SYM(SPEC `k:num` (CONJUNCT1 Y_CLAUSES))) THEN
1980     ASM_SIMP_TAC[Y_INCREASES_LT; ARITH_RULE `0 < n + 1`];
1981     ALL_TAC] THEN
1982   MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN
1983   EXISTS_TAC `abs(&(Y k (n + 1)))` THEN
1984   REWRITE_TAC[GSYM REAL_ABS_MUL; REAL_SUB_LDISTRIB] THEN
1985   ASM_SIMP_TAC[REAL_ABS_NUM; REAL_LT_IMP_NZ;
1986                REAL_OF_NUM_LT; REAL_DIV_LMUL] THEN
1987   REWRITE_TAC[real_div; REAL_MUL_LID; REAL_MUL_ASSOC] THEN
1988   SIMP_TAC[GSYM real_div; REAL_OF_NUM_LT; ARITH; REAL_LT_RDIV_EQ] THEN
1989   MATCH_MP_TAC(REAL_ARITH
1990    `!lx ly ux uy.
1991         lx <= x /\ x <= ux /\ ly <= y /\ y <= uy /\
1992         &2 * uy < &2 * lx + d /\ &2 * ux < &2 * ly + d
1993         ==> abs(x - y) * &2 < d`) THEN
1994   MAP_EVERY EXISTS_TAC
1995    [`&((2 * a * k - 1) EXP n)`; `&((2 * k - 1) EXP n) * &a pow n`;
1996     `&((2 * a * k) EXP n)`; `&((2 * k) EXP n) * &a pow n`] THEN
1997   ASM_SIMP_TAC[REAL_OF_NUM_LE; Y_LOWERBOUND; Y_UPPERBOUND;
1998                REAL_LE_RMUL_EQ; REAL_POW_LT; REAL_OF_NUM_LT;
1999                ARITH_RULE `~(a = 0) ==> 0 < a`] THEN
2000   REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_POW; REAL_OF_NUM_MUL] THEN
2001   REWRITE_TAC[REAL_OF_NUM_LT] THEN
2002   MATCH_MP_TAC(ARITH_RULE
2003    `!x:num. x <= c /\ a < b + x /\ d < e + x ==> a < b + c /\ d < e + c`) THEN
2004   EXISTS_TAC `(2 * k - 1) EXP n` THEN REWRITE_TAC[Y_LOWERBOUND] THEN
2005   REWRITE_TAC[GSYM MULT_EXP; GSYM MULT_ASSOC] THEN
2006   REWRITE_TAC[RIGHT_SUB_DISTRIB; GSYM MULT_ASSOC] THEN
2007   SUBST1_TAC(AC MULT_AC `2 * k * a = 2 * a * k`) THEN
2008   REWRITE_TAC[MULT_CLAUSES] THEN
2009   MATCH_MP_TAC(ARITH_RULE
2010    `b' <= b /\ a < b' + c ==> a < b + c /\ a < b' + c:num`) THEN
2011   CONJ_TAC THENL
2012    [REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
2013     SPEC_TAC(`n:num`,`m:num`) THEN
2014     INDUCT_TAC THEN REWRITE_TAC[CONJUNCT1 EXP; LE_REFL] THEN
2015     REWRITE_TAC[EXP_MONO_LE_SUC] THEN UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC;
2016     ALL_TAC] THEN
2017   SUBST1_TAC(AC MULT_AC `2 * a * k = 2 * k * a`) THEN
2018   GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV o LAND_CONV o RAND_CONV)
2019    [ARITH_RULE `a = 1 * a`] THEN
2020   REWRITE_TAC[MULT_ASSOC; GSYM RIGHT_SUB_DISTRIB] THEN
2021   REWRITE_TAC[MULT_EXP] THEN
2022   REWRITE_TAC[ARITH_RULE `2 * e * a + e = (2 * a + 1) * e`] THEN
2023   REWRITE_TAC[GSYM MULT_EXP; GSYM MULT_ASSOC] THEN
2024   SUBST1_TAC(AC MULT_AC `2 * k * a = a * 2 * k`) THEN
2025   ONCE_REWRITE_TAC[MULT_EXP] THEN REWRITE_TAC[MULT_ASSOC] THEN
2026   SUBGOAL_THEN `(2 * k) * (2 * a EXP n) * (2 * k) EXP n <
2027                 (2 * k) * (2 * a EXP n + 1) * (2 * k - 1) EXP n`
2028   MP_TAC THENL
2029    [ALL_TAC; ASM_SIMP_TAC[LT_MULT_LCANCEL; MULT_EQ_0; ARITH_EQ]] THEN
2030   GEN_REWRITE_TAC RAND_CONV
2031    [AC MULT_AC `(2 * k) * l * m = l * (2 * k) * m`] THEN
2032   MATCH_MP_TAC LTE_TRANS THEN
2033   EXISTS_TAC `(2 * a EXP n + 1) * (2 * k) EXP n * (2 * k - n)` THEN
2034   CONJ_TAC THENL
2035    [ALL_TAC; REWRITE_TAC[LE_MULT_LCANCEL; BINOMIALISH_LEMMA]] THEN
2036   REWRITE_TAC[ARITH_RULE
2037    `(2 * k) * (2 * an) * 2kn < a2na * 2kn * kmn <=>
2038     2kn * 4 * k * an < 2kn * a2na * kmn`] THEN
2039   ASM_SIMP_TAC[LT_MULT_LCANCEL; EXP_EQ_0; MULT_EQ_0; ARITH_EQ] THEN
2040   REWRITE_TAC[LEFT_SUB_DISTRIB] THEN
2041   MATCH_MP_TAC(ARITH_RULE `a + b < c ==> a < c - b:num`) THEN
2042   REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; MULT_CLAUSES] THEN
2043   REWRITE_TAC[GSYM MULT_ASSOC] THEN
2044   REWRITE_TAC[ARITH_RULE `4 * k * an + x < 2 * an * 2 * k + y <=> x < y`] THEN
2045   ONCE_REWRITE_TAC[AC MULT_AC `2 * a * n = 2 * n * a`] THEN
2046   UNDISCH_TAC `2 * n * a EXP n < k` THEN
2047   MATCH_MP_TAC(ARITH_RULE
2048    `n * 1 <= x ==> 2 * x < k ==> 2 * x + n < 2 * k`) THEN
2049   ASM_REWRITE_TAC[LE_MULT_LCANCEL; ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN
2050   ASM_REWRITE_TAC[EXP_EQ_0]);;
2051
2052 let ABS_LT_REPRESENTATION = prove
2053  (`!x y z.
2054     ~(y = 0)
2055     ==> (abs(&x / &y - &z) < &1 / &2 <=>
2056          4 * x EXP 2 + 4 * (y * z) EXP 2 < 8 * x * y * z + y EXP 2)`,
2057   REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
2058   EXISTS_TAC `&4 * (&x / &y - &z) pow 2 < &1` THEN CONJ_TAC THENL
2059    [SIMP_TAC[REAL_LT_RDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
2060     SUBST1_TAC(SYM(REAL_RAT_REDUCE_CONV `&2 * &2`)) THEN
2061     REWRITE_TAC[GSYM REAL_POW_2; GSYM REAL_POW_MUL] THEN
2062     ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
2063     REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM] THEN EQ_TAC THENL
2064      [GEN_REWRITE_TAC (RAND_CONV o RAND_CONV)
2065        [SYM(REAL_RAT_REDUCE_CONV `&1 pow 2`)] THEN
2066       GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN
2067       SIMP_TAC[ARITH_EQ; REAL_POW_LT2; REAL_LE_MUL; REAL_POS; REAL_ABS_POS];
2068       ONCE_REWRITE_TAC[TAUT `a ==> b <=> ~b ==> ~a`] THEN
2069       REWRITE_TAC[REAL_NOT_LT] THEN
2070       GEN_REWRITE_TAC (RAND_CONV o LAND_CONV)
2071        [SYM(REAL_RAT_REDUCE_CONV `&1 pow 2`)] THEN
2072       GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [REAL_MUL_SYM] THEN
2073       SIMP_TAC[ARITH_EQ; REAL_POW_LE2; REAL_LE_MUL; REAL_POS; REAL_ABS_POS]];
2074     ALL_TAC] THEN
2075   MATCH_MP_TAC EQ_TRANS THEN
2076   EXISTS_TAC `&4 * (&x - &y * &z) pow 2 < &y pow 2` THEN CONJ_TAC THENL
2077    [GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM REAL_POW2_ABS] THEN
2078     REWRITE_TAC[GSYM REAL_ABS_POW] THEN
2079     GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM REAL_MUL_LID] THEN
2080     ASM_SIMP_TAC[GSYM REAL_LT_LDIV_EQ; GSYM REAL_ABS_NZ; REAL_POW_EQ_0;
2081                  ARITH_EQ; REAL_OF_NUM_EQ] THEN
2082     REWRITE_TAC[REAL_ABS_POW; REAL_POW2_ABS] THEN
2083     REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
2084     REWRITE_TAC[GSYM real_div; GSYM REAL_POW_DIV] THEN
2085     AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
2086     AP_THM_TAC THEN AP_TERM_TAC THEN
2087     REWRITE_TAC[real_div; REAL_SUB_RDISTRIB; GSYM REAL_MUL_ASSOC] THEN
2088     AP_TERM_TAC THEN
2089     ASM_SIMP_TAC[GSYM real_div; REAL_DIV_LMUL; REAL_OF_NUM_EQ]; ALL_TAC] THEN
2090   REWRITE_TAC[GSYM REAL_OF_NUM_LT; GSYM REAL_OF_NUM_ADD;
2091               GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_POW] THEN
2092   REWRITE_TAC[REAL_POW_2] THEN REAL_ARITH_TAC);;
2093
2094 let Y_EQ_0 = prove
2095  (`!a n. ~(a = 0) ==> ((Y a n = 0) <=> (n = 0))`,
2096   REPEAT STRIP_TAC THEN
2097   SUBST1_TAC(SYM(SPEC `a:num` (CONJUNCT1 Y_CLAUSES))) THEN
2098   ASM_SIMP_TAC[Y_INJ] THEN REWRITE_TAC[Y_CLAUSES]);;
2099
2100 let XY_EXP = prove
2101  (`~(a = 0)
2102    ==> ((a EXP n = p) <=>
2103         ?k x y z. (Y (a * k) (n + 1) = x) /\
2104                   (Y k (n + 1) = y) /\
2105                   (Y a (n + 1) = z) /\
2106                   2 * n * z < k /\
2107                   4 * x EXP 2 + 4 * (y * p) EXP 2 < 8 * x * y * p + y EXP 2)`,
2108   let lemma1 = prove
2109    (`(?x y z. (a = x) /\ (b = y) /\ (c = z) /\ P x y z) <=> P a b c`,
2110     MESON_TAC[])
2111   and lemma2 =
2112     CONV_RULE(RAND_CONV(ONCE_DEPTH_CONV SYM_CONV))
2113              (SPEC_ALL ABS_LT_REPRESENTATION) in
2114   REPEAT STRIP_TAC THEN REWRITE_TAC[lemma1] THEN
2115   GEN_REWRITE_TAC (RAND_CONV o BINDER_CONV o LAND_CONV)
2116     [ARITH_RULE `n < k <=> n < k /\ ~(k = 0)`] THEN
2117   ONCE_REWRITE_TAC[TAUT `a /\ b <=> ~(a ==> ~b)`] THEN
2118   ASM_SIMP_TAC[lemma2; Y_EQ_0; ADD_EQ_0; ARITH_EQ] THEN
2119   REWRITE_TAC[NOT_IMP] THEN
2120   REWRITE_TAC[ARITH_RULE `n < k /\ ~(k = 0) <=> n < k`] THEN
2121   EQ_TAC THENL
2122    [DISCH_THEN(SUBST1_TAC o SYM) THEN
2123     EXISTS_TAC `2 * n * Y a (n + 1) + 1` THEN
2124     REWRITE_TAC[ARITH_RULE `c < c + 1`; GSYM REAL_OF_NUM_POW] THEN
2125     MATCH_MP_TAC XY_EXP_LEMMA THEN ASM_REWRITE_TAC[] THEN
2126     MATCH_MP_TAC(ARITH_RULE `a <= b ==> 2 * a < 2 * b + 1`) THEN
2127     REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
2128     MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `(2 * a - 1) EXP n` THEN
2129     REWRITE_TAC[Y_LOWERBOUND] THEN
2130     SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
2131     REWRITE_TAC[CONJUNCT1 EXP; LE_REFL; EXP_MONO_LE_SUC] THEN
2132     UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC; ALL_TAC] THEN
2133   DISCH_THEN(X_CHOOSE_THEN `k:num` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
2134   MP_TAC(SPECL [`a:num`; `k:num`; `n:num`] XY_EXP_LEMMA) THEN
2135   ANTS_TAC THENL
2136    [ASM_REWRITE_TAC[] THEN
2137     FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
2138      `2 * a < k ==> b <= a ==> 2 * b < k`)) THEN
2139     REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
2140     MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `(2 * a - 1) EXP n` THEN
2141     REWRITE_TAC[Y_LOWERBOUND] THEN
2142     SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
2143     REWRITE_TAC[CONJUNCT1 EXP; LE_REFL; EXP_MONO_LE_SUC] THEN
2144     UNDISCH_TAC `~(a = 0)` THEN ARITH_TAC; ALL_TAC] THEN
2145   REWRITE_TAC[IMP_IMP] THEN
2146   DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
2147    `abs(x - a) < e1 /\ abs(x - b) < e2 ==> abs(a - b) < e1 + e2`)) THEN
2148   CONV_TAC REAL_RAT_REDUCE_CONV THEN
2149   DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
2150    `abs(a - b) < &1
2151     ==> a + &1 <= b \/ (a = b) \/ b + &1 <= a ==> (a = b)`)) THEN
2152   REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_ADD;
2153               REAL_OF_NUM_EQ; REAL_OF_NUM_LE] THEN
2154   DISCH_THEN MATCH_MP_TAC THEN ARITH_TAC);;
2155
2156 (* ------------------------------------------------------------------------- *)
2157 (* Lemmas.                                                                   *)
2158 (* ------------------------------------------------------------------------- *)
2159
2160 let REAL_SUM_OF_SQUARES = prove
2161  (`(x pow 2 + y pow 2 = &0) <=> (x = &0) /\ (y = &0)`,
2162   REWRITE_TAC[REAL_POW_2] THEN EQ_TAC THEN
2163   SIMP_TAC[REAL_MUL_LZERO; REAL_ADD_LID] THEN
2164   DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
2165    `(a + b = &0) ==> &0 <= a /\ &0 <= b ==> (a = &0) /\ (b = &0)`)) THEN
2166   REWRITE_TAC[REAL_LE_SQUARE; REAL_ENTIRE]);;
2167
2168 (* ------------------------------------------------------------------------- *)
2169 (* Combining theorems for conjunction and disjunction.                       *)
2170 (* ------------------------------------------------------------------------- *)
2171
2172 let DIOPH_CONJ = prove
2173  (`(x1 = x2) /\ (y1 = y2) <=>
2174    (x1 * x1 + x2 * x2 + y1 * y1 + y2 * y2 = 2 * x1 * x2 + 2 * y1 * y2)`,
2175   REWRITE_TAC[GSYM REAL_OF_NUM_EQ;
2176     GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL] THEN
2177   ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN
2178   REWRITE_TAC[GSYM REAL_SUM_OF_SQUARES] THEN
2179   REWRITE_TAC[REAL_POW_2] THEN REAL_ARITH_TAC);;
2180
2181 let DIOPH_DISJ = prove
2182  (`(x1 = x2) \/ (y1 = y2) <=>
2183    (x1 * y1 + x2 * y2 = x1 * y2 + x2 * y1)`,
2184   REWRITE_TAC[GSYM REAL_OF_NUM_EQ;
2185     GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_MUL] THEN
2186   ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN
2187   REWRITE_TAC[GSYM REAL_ENTIRE] THEN REAL_ARITH_TAC);;
2188
2189 (* ------------------------------------------------------------------------- *)
2190 (* Inequalities.                                                             *)
2191 (* ------------------------------------------------------------------------- *)
2192
2193 let DIOPH_LE = prove
2194  (`x <= y <=> ?d:num. x + d = y`,
2195   REWRITE_TAC[LE_EXISTS] THEN
2196   AP_TERM_TAC THEN ABS_TAC THEN
2197   REWRITE_TAC[ADD_AC; EQ_SYM_EQ]);;
2198
2199 let DIOPH_LT = prove
2200  (`x < y <=> ?d. x + d + 1 = y`,
2201   REWRITE_TAC[LT_EXISTS] THEN
2202   REWRITE_TAC[ADD1] THEN
2203   AP_TERM_TAC THEN ABS_TAC THEN
2204   REWRITE_TAC[ADD_AC; EQ_SYM_EQ]);;
2205
2206 let DIOPH_NE = prove
2207  (`~(x = y) <=> x < y \/ y < x:num`,
2208   ARITH_TAC);;
2209
2210 (* ------------------------------------------------------------------------- *)
2211 (* Exponentiation (from the Pell stuff).                                     *)
2212 (* ------------------------------------------------------------------------- *)
2213
2214 let Y_0 = prove
2215  (`!k. Y 0 k = if k = 1 then 1 else 0`,
2216   INDUCT_TAC THEN REWRITE_TAC[Y_CLAUSES; ARITH_EQ] THEN
2217   SPEC_TAC(`k:num`,`k:num`) THEN
2218   INDUCT_TAC THEN REWRITE_TAC[Y_CLAUSES; ARITH] THEN
2219   REWRITE_TAC[ARITH_RULE `SUC(SUC n) = n + 2`; Y_CLAUSES; ARITH] THEN
2220   REWRITE_TAC[MULT_CLAUSES; SUB_0; ARITH_RULE `~(k + 2 = 1)`]);;
2221
2222 let Y_0_TRIV = prove
2223  (`!k. (Y 0 k = 0) <=> ~(k = 1)`,
2224   GEN_TAC THEN REWRITE_TAC[Y_0] THEN
2225   COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH_EQ]);;
2226
2227 let DIOPH_Y = prove
2228  (`(Y a k = y) <=>
2229         (a = 0) /\ (k = 1) /\ (y = 1) \/
2230         (a = 0) /\ ~(k = 1) /\ (y = 0) \/
2231         (k = 0) /\ (y = 0) \/
2232         (a = 1) /\ (y = k) \/
2233         ~(a = 0) /\ ~(k = 0) /\ ~(a = 1) /\ ~(y = 0) /\
2234         ?x u v r b p q s t c d.
2235                 0 < r /\
2236                 (x EXP 2 = (a EXP 2 - 1) * y EXP 2 + 1) /\
2237                 (u EXP 2 = (a EXP 2 - 1) * v EXP 2 + 1) /\
2238                 (s EXP 2 = (b EXP 2 - 1) * t EXP 2 + 1) /\
2239                 (v = r * y EXP 2) /\
2240                 (b = 1 + 4 * p * y) /\
2241                 (b = a + q * u) /\
2242                 (s = x + c * u) /\
2243                 (t = k + 4 * d * y) /\
2244                 k <= y`,
2245   ASM_CASES_TAC `a = 0` THENL
2246    [ASM_CASES_TAC `y = 0` THENL
2247      [ASM_REWRITE_TAC[Y_0_TRIV; ARITH_EQ] THEN ARITH_TAC; ALL_TAC] THEN
2248     ASM_CASES_TAC `k = 0` THEN ASM_REWRITE_TAC[Y_CLAUSES; ARITH_EQ] THEN
2249     ASM_REWRITE_TAC[ARITH_EQ] THEN CONV_TAC NUM_REDUCE_CONV THEN
2250     REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES] THEN
2251     REWRITE_TAC[EXP_2; MULT_EQ_1] THEN
2252     REWRITE_TAC[Y_0] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
2253     REWRITE_TAC[EQ_SYM_EQ]; ALL_TAC] THEN
2254   ASM_REWRITE_TAC[ARITH_EQ] THEN
2255   ASM_CASES_TAC `k = 0` THEN ASM_REWRITE_TAC[Y_CLAUSES] THENL
2256    [REWRITE_TAC[EQ_SYM_EQ] THEN CONV_TAC(EQT_INTRO o TAUT); ALL_TAC] THEN
2257   ASM_CASES_TAC `a = 1` THEN ASM_REWRITE_TAC[Y_DEGENERATE] THENL
2258    [REWRITE_TAC[EQ_SYM_EQ]; ALL_TAC] THEN
2259   ASM_CASES_TAC `y = 0` THEN ASM_SIMP_TAC[Y_EQ_0] THEN
2260   GEN_REWRITE_TAC LAND_CONV [EQ_SYM_EQ] THEN ASM_SIMP_TAC[Y_DIOPH]);;
2261
2262 let DIOPH_EXP_LEMMA = prove
2263  (`(m EXP n = p) <=>
2264         (m = 0) /\ (n = 0) /\ (p = 1) \/
2265         (m = 0) /\ ~(n = 0) /\ (p = 0) \/
2266         ~(m = 0) /\
2267         ?k x y z. (Y (m * k) (n + 1) = x) /\
2268                   (Y k (n + 1) = y) /\
2269                   (Y m (n + 1) = z) /\
2270                   2 * n * z < k /\
2271                   4 * x EXP 2 + 4 * (y * p) EXP 2 < 8 * x * y * p + y EXP 2`,
2272   ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[ARITH_EQ] THENL
2273    [SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
2274     REWRITE_TAC[EXP; MULT_CLAUSES; ADD_CLAUSES; NOT_SUC] THEN
2275     REWRITE_TAC[EQ_SYM_EQ]; ALL_TAC] THEN
2276   ASM_SIMP_TAC[XY_EXP]);;
2277
2278 let DIOPH_EXP =
2279   let th1 = REWRITE_RULE[DIOPH_Y] DIOPH_EXP_LEMMA in
2280   let th2 = REWRITE_RULE[EXP_2] th1 in
2281   let th3 = REWRITE_RULE[DIOPH_NE; DIOPH_LT; DIOPH_LE] th2 in
2282   let th4 = REWRITE_RULE[ADD_CLAUSES; ARITH_EQ; ADD_EQ_0;
2283     ARITH_RULE `(n + 1 = 1) = (n = 0)`; ADD_ASSOC;
2284     EQ_ADD_RCANCEL] th3 in
2285   let th5 = REWRITE_RULE[GSYM ADD_ASSOC] th4 in
2286   REWRITE_RULE
2287    [OR_EXISTS_THM; LEFT_OR_EXISTS_THM; RIGHT_OR_EXISTS_THM;
2288     LEFT_AND_EXISTS_THM; RIGHT_AND_EXISTS_THM] th5;;
2289
2290 (****** This takes about an hour to compute, and longer to print out!
2291
2292 let DIOPH_EXP_ONE_EQUATION =
2293   REWRITE_RULE[DIOPH_CONJ; DIOPH_DISJ] DIOPH_EXP;;
2294
2295  *******)