(* ========================================================================= *)
(* Basic divisibility notions over the integers.                             *)
(*                                                                           *)
(* This is similar to stuff in Library/prime.ml etc. for natural numbers.    *)
(* ========================================================================= *)

prioritize_int();;

(* ------------------------------------------------------------------------- *)
(* Basic properties of divisibility.                                         *)
(* ------------------------------------------------------------------------- *)

let INT_DIVIDES_REFL = INTEGER_RULE
  `!d. d divides d`;;

let INT_DIVIDES_TRANS = INTEGER_RULE
  `!x y z. x divides y /\ y divides z ==> x divides z`;;

let INT_DIVIDES_ADD = INTEGER_RULE
  `!d a b. d divides a /\ d divides b ==> d divides (a + b)`;;

let INT_DIVIDES_SUB = INTEGER_RULE
  `!d a b. d divides a /\ d divides b ==> d divides (a - b)`;;

let INT_DIVIDES_0 = INTEGER_RULE
  `!d. d divides &0`;;

let INT_DIVIDES_ZERO = INTEGER_RULE
  `!x. &0 divides x <=> x = &0`;;

let INT_DIVIDES_LNEG = INTEGER_RULE
  `!d x. (--d) divides x <=> d divides x`;;

let INT_DIVIDES_RNEG = INTEGER_RULE
  `!d x. d divides (--x) <=> d divides x`;;

let INT_DIVIDES_RMUL = INTEGER_RULE
  `!d x y. d divides x ==> d divides (x * y)`;;

let INT_DIVIDES_LMUL = INTEGER_RULE
  `!d x y. d divides y ==> d divides (x * y)`;;

let INT_DIVIDES_1 = INTEGER_RULE
  `!x. &1 divides x`;;

let INT_DIVIDES_ADD_REVR = INTEGER_RULE
  `!d a b. d divides a /\ d divides (a + b) ==> d divides b`;;

let INT_DIVIDES_ADD_REVL = INTEGER_RULE
  `!d a b. d divides b /\ d divides (a + b) ==> d divides a`;;

let INT_DIVIDES_MUL_L = INTEGER_RULE
  `!a b c. a divides b ==> (c * a) divides (c * b)`;;

let INT_DIVIDES_MUL_R = INTEGER_RULE
  `!a b c. a divides b ==> (a * c) divides (b * c)`;;

let INT_DIVIDES_LMUL2 = INTEGER_RULE
  `!d a x. (x * d) divides a ==> d divides a`;;

let INT_DIVIDES_RMUL2 = INTEGER_RULE
  `!d a x. (d * x) divides a ==> d divides a`;;

let INT_DIVIDES_CMUL2 = INTEGER_RULE
  `!a b c. (c * a) divides (c * b) /\ ~(c = &0) ==> a divides b`;;

let INT_DIVIDES_LMUL2_EQ = INTEGER_RULE
  `!a b c. ~(c = &0) ==> ((c * a) divides (c * b) <=> a divides b)`;;

let INT_DIVIDES_RMUL2_EQ = INTEGER_RULE
  `!a b c. ~(c = &0) ==> ((a * c) divides (b * c) <=> a divides b)`;;

let INT_DIVIDES_MUL2 = INTEGER_RULE
  `!a b c d. a divides b /\ c divides d ==> (a * c) divides (b * d)`;;


let INT_DIVIDES_LABS = 
prove
 (`!d n. abs(d) divides n <=> d divides n`,

  REPEAT GEN_TAC THEN SIMP_TAC[INT_ABS] THEN COND_CASES_TAC THEN INTEGER_TAC);;


let INT_DIVIDES_RABS = 
prove
 (`!d n. d divides (abs n) <=> d divides n`,

  REPEAT GEN_TAC THEN SIMP_TAC[INT_ABS] THEN COND_CASES_TAC THEN INTEGER_TAC);;


let INT_DIVIDES_ABS = 
prove
 (`(!d n. abs(d) divides n <=> d divides n) /\
   (!d n. d divides (abs n) <=> d divides n)`,


let INT_DIVIDES_POW = 
prove
 (`!x y n. x divides y ==> (x pow n) divides (y pow n)`,

  REWRITE_TAC[int_divides] THEN MESON_TAC[INT_POW_MUL]);;


let INT_DIVIDES_POW2 = 
prove
 (`!n x y. ~(n = 0) /\ (x pow n) divides y ==> x divides y`,

  INDUCT_TAC THEN REWRITE_TAC[NOT_SUC; INT_POW] THEN INTEGER_TAC);;


let INT_DIVIDES_RPOW = 
prove
 (`!x y n. x divides y /\ ~(n = 0) ==> x divides (y pow n)`,

  GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
  SIMP_TAC[INT_DIVIDES_RMUL; INT_POW]);;


let INT_DIVIDES_RPOW_SUC = 
prove
 (`!x y n. x divides y ==> x divides (y pow (SUC n))`,

  SIMP_TAC[INT_DIVIDES_RPOW; NOT_SUC]);;


let INT_DIVIDES_ANTISYM_DIVISORS = 
prove
 (`!a b:int. a divides b /\ b divides a <=> !d. d divides a <=> d divides b`,

  MESON_TAC[INT_DIVIDES_REFL; INT_DIVIDES_TRANS]);;

(* ------------------------------------------------------------------------- *)
(* Now carefully distinguish signs.                                          *)
(* ------------------------------------------------------------------------- *)


let INT_DIVIDES_ONE_POS = 
prove
 (`!x. &0 <= x ==> (x divides &1 <=> x = &1)`,

  REPEAT STRIP_TAC THEN EQ_TAC THENL
   [REWRITE_TAC[int_divides]; INTEGER_TAC] THEN
  DISCH_THEN(CHOOSE_THEN(MP_TAC o AP_TERM `abs` o SYM)) THEN
  SIMP_TAC[INT_ABS_NUM; INT_ABS_MUL_1] THEN ASM_SIMP_TAC[INT_ABS]);;


let INT_DIVIDES_ONE_ABS = 
prove
 (`!d. d divides &1 <=> abs(d) = &1`,


let INT_DIVIDES_ONE = 
prove
 (`!d. d divides &1 <=> d = &1 \/ d = -- &1`,

  REWRITE_TAC[INT_DIVIDES_ONE_ABS] THEN INT_ARITH_TAC);;


let INT_DIVIDES_ANTISYM_ASSOCIATED = 
prove
 (`!x y. x divides y /\ y divides x <=> ?u. u divides &1 /\ x = y * u`,

  REPEAT GEN_TAC THEN EQ_TAC THENL [ALL_TAC; INTEGER_TAC] THEN
  ASM_CASES_TAC `x = &0` THEN ASM_SIMP_TAC[INT_DIVIDES_ZERO; INT_MUL_LZERO] THEN
  ASM_MESON_TAC[int_divides; INT_DIVIDES_REFL;
    INTEGER_RULE `y = x * d /\ x = y * e /\ ~(y = &0) ==> d divides &1`]);;


let INT_DIVIDES_ANTISYM = 
prove
 (`!x y. x divides y /\ y divides x <=> x = y \/ x = --y`,

  REWRITE_TAC[INT_DIVIDES_ANTISYM_ASSOCIATED; INT_DIVIDES_ONE] THEN
  REWRITE_TAC[RIGHT_OR_DISTRIB; EXISTS_OR_THM; UNWIND_THM2] THEN
  INT_ARITH_TAC);;


let INT_DIVIDES_ANTISYM_ABS = 
prove
 (`!x y. x divides y /\ y divides x <=> abs(x) = abs(y)`,

  REWRITE_TAC[INT_DIVIDES_ANTISYM] THEN INT_ARITH_TAC);;


let INT_DIVIDES_ANTISYM_POS = 
prove
 (`!x y. &0 <= x /\ &0 <= y ==> (x divides y /\ y divides x <=> x = y)`,

  REWRITE_TAC[INT_DIVIDES_ANTISYM_ABS] THEN INT_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* Lemmas about GCDs.                                                        *)
(* ------------------------------------------------------------------------- *)


let INT_GCD_POS = 
prove
 (`!a b. &0 <= gcd(a,b)`,

  REWRITE_TAC[int_gcd]);;


let INT_GCD_DIVIDES = 
prove
 (`!a b. gcd(a,b) divides a /\ gcd(a,b) divides b`,

  INTEGER_TAC);;


let INT_GCD_BEZOUT = 
prove
 (`!a b. ?x y. gcd(a,b) = a * x + b * y`,

  INTEGER_TAC);;


let INT_DIVIDES_GCD = 
prove
 (`!a b d. d divides gcd(a,b) <=> d divides a /\ d divides b`,

  INTEGER_TAC);;


let INT_DIVIDES_GCD = 
prove
 (`!a b d. d divides gcd(a,b) <=> d divides a /\ d divides b`,

  INTEGER_TAC);;

let INT_GCD = INTEGER_RULE
  `!a b. (gcd(a,b) divides a /\ gcd(a,b) divides b) /\
         (!e. e divides a /\ e divides b ==> e divides gcd(a,b))`;;


let INT_GCD_UNIQUE = 
prove
 (`!a b d. gcd(a,b) = d <=> &0 <= d /\ d divides a /\ d divides b /\
                            !e. e divides a /\ e divides b ==> e divides d`,

  REPEAT GEN_TAC THEN EQ_TAC THENL
   [MESON_TAC[INT_GCD; INT_GCD_POS]; ALL_TAC] THEN
  ASM_SIMP_TAC[INT_GCD_POS; GSYM INT_DIVIDES_ANTISYM_POS; INT_DIVIDES_GCD] THEN
  REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN INTEGER_TAC);;


let INT_GCD_UNIQUE_ABS = 
prove
 (`!a b d. gcd(a,b) = abs(d) <=>
           d divides a /\ d divides b /\
           !e. e divides a /\ e divides b ==> e divides d`,


let INT_GCD_REFL = 
prove
 (`!a. gcd(a,a) = abs(a)`,

  REWRITE_TAC[INT_GCD_UNIQUE_ABS] THEN INTEGER_TAC);;


let INT_GCD_SYM = 
prove
 (`!a b. gcd(a,b) = gcd(b,a)`,

  SIMP_TAC[INT_GCD_POS; GSYM INT_DIVIDES_ANTISYM_POS] THEN INTEGER_TAC);;


let INT_GCD_ASSOC = 
prove
 (`!a b c. gcd(a,gcd(b,c)) = gcd(gcd(a,b),c)`,

  SIMP_TAC[INT_GCD_POS; GSYM INT_DIVIDES_ANTISYM_POS] THEN INTEGER_TAC);;


let INT_GCD_1 = 
prove
 (`!a. gcd(a,&1) = &1 /\ gcd(&1,a) = &1`,

  SIMP_TAC[INT_GCD_UNIQUE; INT_POS; INT_DIVIDES_1]);;


let INT_GCD_0 = 
prove
 (`!a. gcd(a,&0) = abs(a) /\ gcd(&0,a) = abs(a)`,

  SIMP_TAC[INT_GCD_UNIQUE_ABS] THEN INTEGER_TAC);;


let INT_GCD_ABS = 
prove
 (`!a b. gcd(abs(a),b) = gcd(a,b) /\ gcd(a,abs(b)) = gcd(a,b)`,

  REWRITE_TAC[INT_GCD_UNIQUE; INT_DIVIDES_ABS; INT_GCD_POS; INT_GCD]);;

let INT_GCD_MULTIPLE =
 (`!a b. gcd(a,a * b) = abs(a) /\ gcd(b,a * b) = abs(b)`,
  REWRITE_TAC[INT_GCD_UNIQUE_ABS] THEN INTEGER_TAC);;


let INT_GCD_ADD = 
prove
 (`(!a b. gcd(a + b,b) = gcd(a,b)) /\
   (!a b. gcd(b + a,b) = gcd(a,b)) /\
   (!a b. gcd(a,a + b) = gcd(a,b)) /\
   (!a b. gcd(a,b + a) = gcd(a,b))`,

  SIMP_TAC[INT_GCD_UNIQUE; INT_GCD_POS] THEN INTEGER_TAC);;


let INT_GCD_SUB = 
prove
 (`(!a b. gcd(a - b,b) = gcd(a,b)) /\
   (!a b. gcd(b - a,b) = gcd(a,b)) /\
   (!a b. gcd(a,a - b) = gcd(a,b)) /\
   (!a b. gcd(a,b - a) = gcd(a,b))`,

  SIMP_TAC[INT_GCD_UNIQUE; INT_GCD_POS] THEN INTEGER_TAC);;


let INT_DIVIDES_GCD_LEFT = 
prove
 (`!m n:int. m divides n <=> gcd(m,n) = abs m`,

  SIMP_TAC[INT_GCD_UNIQUE; INT_ABS_POS; INT_DIVIDES_ABS; INT_DIVIDES_REFL] THEN
  MESON_TAC[INT_DIVIDES_REFL; INT_DIVIDES_TRANS]);;


let INT_DIVIDES_GCD_RIGHT = 
prove
 (`!m n:int. n divides m <=> gcd(m,n) = abs n`,

  SIMP_TAC[INT_GCD_UNIQUE; INT_ABS_POS; INT_DIVIDES_ABS; INT_DIVIDES_REFL] THEN
  MESON_TAC[INT_DIVIDES_REFL; INT_DIVIDES_TRANS]);;

(* ------------------------------------------------------------------------- *)
(* More lemmas about coprimality.                                            *)
(* ------------------------------------------------------------------------- *)


let INT_COPRIME_GCD = 
prove
 (`!a b. coprime(a,b) <=> gcd(a,b) = &1`,

  SIMP_TAC[GSYM INT_DIVIDES_ONE_POS; INT_GCD_POS] THEN INTEGER_TAC);;


let int_coprime = 
prove
 (`!a b. coprime(a,b) <=> !d. d divides a /\ d divides b ==> d divides &1`,

  REWRITE_TAC[INT_COPRIME_GCD; INT_GCD_UNIQUE; INT_POS; INT_DIVIDES_1]);;


let COPRIME = 
prove
 (`!a b. coprime(a,b) <=> !d. d divides a /\ d divides b <=> d divides &1`,

  MESON_TAC[INT_DIVIDES_1; INT_DIVIDES_TRANS; int_coprime]);;


let INT_COPRIME_SYM = 
prove
 (`!a b. coprime(a,b) <=> coprime(b,a)`,

  INTEGER_TAC);;


let INT_COPRIME_DIVPROD = 
prove
 (`!d a b. d divides (a * b) /\ coprime(d,a) ==> d divides b`,

  INTEGER_TAC);;


let INT_COPRIME_1 = 
prove
 (`!a. coprime(a,&1) /\ coprime(&1,a)`,

  INTEGER_TAC);;


let INT_GCD_COPRIME = 
prove
 (`!a b a' b'. ~(gcd(a,b) = &0) /\ a = a' * gcd(a,b) /\ b = b' * gcd(a,b)
               ==> coprime(a',b')`,

  INTEGER_TAC);;


let INT_GCD_COPRIME_EXISTS = 
prove
 (`!a b. ~(gcd(a,b) = &0) ==>
        ?a' b'. (a = a' * gcd(a,b)) /\
                (b = b' * gcd(a,b)) /\
                coprime(a',b')`,

  INTEGER_TAC);;


let INT_COPRIME_0 = 
prove
 (`(!a. coprime(a,&0) <=> a divides &1) /\
   (!a. coprime(&0,a) <=> a divides &1)`,

  INTEGER_TAC);;


let INT_COPRIME_MUL = 
prove
 (`!d a b. coprime(d,a) /\ coprime(d,b) ==> coprime(d,a * b)`,

  INTEGER_TAC);;


let INT_COPRIME_LMUL2 = 
prove
 (`!d a b. coprime(d,a * b) ==> coprime(d,b)`,

  INTEGER_TAC);;


let INT_COPRIME_RMUL2 = 
prove
 (`!d a b.  coprime(d,a * b) ==> coprime(d,a)`,

  INTEGER_TAC);;


let INT_COPRIME_LMUL = 
prove
 (`!d a b. coprime(a * b,d) <=> coprime(a,d) /\ coprime(b,d)`,

  INTEGER_TAC);;


let INT_COPRIME_RMUL = 
prove
 (`!d a b. coprime(d,a * b) <=> coprime(d,a) /\ coprime(d,b)`,

  INTEGER_TAC);;


let INT_COPRIME_REFL = 
prove
 (`!n. coprime(n,n) <=> n divides &1`,

  INTEGER_TAC);;


let INT_COPRIME_PLUS1 = 
prove
 (`!n. coprime(n + &1,n) /\ coprime(n,n + &1)`,

  INTEGER_TAC);;


let INT_COPRIME_MINUS1 = 
prove
 (`!n. coprime(n - &1,n) /\ coprime(n,n - &1)`,

  INTEGER_TAC);;


let INT_COPRIME_RPOW = 
prove
 (`!m n k. coprime(m,n pow k) <=> coprime(m,n) \/ k = 0`,

  GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
  ASM_SIMP_TAC[INT_POW; INT_COPRIME_1; INT_COPRIME_RMUL; NOT_SUC] THEN
  CONV_TAC TAUT);;


let INT_COPRIME_LPOW = 
prove
 (`!m n k. coprime(m pow k,n) <=> coprime(m,n) \/ k = 0`,

  ONCE_REWRITE_TAC[INT_COPRIME_SYM] THEN REWRITE_TAC[INT_COPRIME_RPOW]);;


let INT_COPRIME_POW2 = 
prove
 (`!m n k. coprime(m pow k,n pow k) <=> coprime(m,n) \/ k = 0`,


let INT_COPRIME_POW = 
prove
 (`!n a d. coprime(d,a) ==> coprime(d,a pow n)`,

  SIMP_TAC[INT_COPRIME_RPOW]);;


let INT_COPRIME_POW_IMP = 
prove
 (`!n a b. coprime(a,b) ==> coprime(a pow n,b pow n)`,


let INT_GCD_EQ_0 = 
prove
 (`!a b. gcd(a,b) = &0 <=> a = &0 /\ b = &0`,

  INTEGER_TAC);;


let INT_DIVISION_DECOMP = 
prove
 (`!a b c. a divides (b * c)
           ==> ?b' c'. (a = b' * c') /\ b' divides b /\ c' divides c`,

  REPEAT STRIP_TAC THEN EXISTS_TAC `gcd(a,b)` THEN
  ASM_CASES_TAC `gcd(a,b) = &0` THEN REPEAT(POP_ASSUM MP_TAC) THENL
   [SIMP_TAC[INT_GCD_EQ_0; INT_GCD_0; INT_ABS_NUM]; INTEGER_TAC] THEN
  REWRITE_TAC[INT_MUL_LZERO] THEN MESON_TAC[INT_DIVIDES_REFL]);;


let INT_DIVIDES_MUL = 
prove
 (`!m n r. m divides r /\ n divides r /\ coprime(m,n) ==> (m * n) divides r`,

  INTEGER_TAC);;


let INT_CHINESE_REMAINDER = 
prove
 (`!a b u v. coprime(a,b) /\ ~(a = &0) /\ ~(b = &0)
             ==> ?x q1 q2. (x = u + q1 * a) /\ (x = v + q2 * b)`,

  INTEGER_TAC);;


let INT_CHINESE_REMAINDER_USUAL = 
prove
 (`!a b u v. coprime(a,b) ==> ?x. (x == u) (mod a) /\ (x == v) (mod b)`,

  INTEGER_TAC);;


let INT_COPRIME_DIVISORS = 
prove
 (`!a b d e. d divides a /\ e divides b /\ coprime(a,b) ==> coprime(d,e)`,

  INTEGER_TAC);;


let INT_COPRIME_LNEG = 
prove
 (`!a b. coprime(--a,b) <=> coprime(a,b)`,

  INTEGER_TAC);;


let INT_COPRIME_RNEG = 
prove
 (`!a b. coprime(a,--b) <=> coprime(a,b)`,

  INTEGER_TAC);;


let INT_COPRIME_NEG = 
prove
 (`(!a b. coprime(--a,b) <=> coprime(a,b)) /\
   (!a b. coprime(a,--b) <=> coprime(a,b))`,

  INTEGER_TAC);;


let INT_COPRIME_LABS = 
prove
 (`!a b. coprime(abs a,b) <=> coprime(a,b)`,

  REWRITE_TAC[INT_ABS] THEN MESON_TAC[INT_COPRIME_LNEG]);;


let INT_COPRIME_RABS = 
prove
 (`!a b. coprime(a,abs b) <=> coprime(a,b)`,

  REWRITE_TAC[INT_ABS] THEN MESON_TAC[INT_COPRIME_RNEG]);;


let INT_COPRIME_ABS = 
prove
 (`(!a b. coprime(abs a,b) <=> coprime(a,b)) /\
   (!a b. coprime(a,abs b) <=> coprime(a,b))`,

(* ------------------------------------------------------------------------- *)
(* More lemmas about congruences.                                            *)
(* ------------------------------------------------------------------------- *)


let INT_CONG_MOD_0 = 
prove
 (`!x y. (x == y) (mod &0) <=> (x = y)`,

  INTEGER_TAC);;


let INT_CONG_MOD_1 = 
prove
 (`!x y. (x == y) (mod &1)`,

  INTEGER_TAC);;


let INT_CONG_0 = 
prove
 (`!x n. ((x == &0) (mod n) <=> n divides x)`,

  INTEGER_TAC);;


let INT_CONG = 
prove
 (`!x y n. (x == y) (mod n) <=> n divides (x - y)`,

  INTEGER_TAC);;


let INT_CONG_MUL_LCANCEL = 
prove
 (`!a n x y. coprime(a,n) /\ (a * x == a * y) (mod n) ==> (x == y) (mod n)`,

  INTEGER_TAC);;


let INT_CONG_MUL_RCANCEL = 
prove
 (`!a n x y. coprime(a,n) /\ (x * a == y * a) (mod n) ==> (x == y) (mod n)`,

  INTEGER_TAC);;


let INT_CONG_REFL = 
prove
 (`!x n. (x == x) (mod n)`,

  INTEGER_TAC);;


let INT_EQ_IMP_CONG = 
prove
 (`!a b n. a = b ==> (a == b) (mod n)`,

  INTEGER_TAC);;


let INT_CONG_SYM = 
prove
 (`!x y n. (x == y) (mod n) <=> (y == x) (mod n)`,

  INTEGER_TAC);;


let INT_CONG_TRANS = 
prove
 (`!x y z n. (x == y) (mod n) /\ (y == z) (mod n) ==> (x == z) (mod n)`,

  INTEGER_TAC);;


let INT_CONG_ADD = 
prove
 (`!x x' y y'.
     (x == x') (mod n) /\ (y == y') (mod n) ==> (x + y == x' + y') (mod n)`,

  INTEGER_TAC);;


let INT_CONG_SUB = 
prove
 (`!x x' y y'.
     (x == x') (mod n) /\ (y == y') (mod n) ==> (x - y == x' - y') (mod n)`,

  INTEGER_TAC);;


let INT_CONG_MUL = 
prove
 (`!x x' y y'.
     (x == x') (mod n) /\ (y == y') (mod n) ==> (x * y == x' * y') (mod n)`,

  INTEGER_TAC);;


let INT_CONG_POW = 
prove
 (`!n k x y. (x == y) (mod n) ==> (x pow k == y pow k) (mod n)`,

  GEN_TAC THEN INDUCT_TAC THEN
  ASM_SIMP_TAC[INT_CONG_MUL; INT_POW; INT_CONG_REFL]);;


let INT_CONG_MUL_LCANCEL_EQ = 
prove
 (`!a n x y. coprime(a,n) ==> ((a * x == a * y) (mod n) <=> (x == y) (mod n))`,

  INTEGER_TAC);;


let INT_CONG_MUL_RCANCEL_EQ = 
prove
 (`!a n x y. coprime(a,n) ==> ((x * a == y * a) (mod n) <=> (x == y) (mod n))`,

  INTEGER_TAC);;


let INT_CONG_ADD_LCANCEL_EQ = 
prove
 (`!a n x y. (a + x == a + y) (mod n) <=> (x == y) (mod n)`,

  INTEGER_TAC);;


let INT_CONG_ADD_RCANCEL_EQ = 
prove
 (`!a n x y. (x + a == y + a) (mod n) <=> (x == y) (mod n)`,

  INTEGER_TAC);;


let INT_CONG_ADD_RCANCEL = 
prove
 (`!a n x y. (x + a == y + a) (mod n) ==> (x == y) (mod n)`,

  INTEGER_TAC);;


let INT_CONG_ADD_LCANCEL = 
prove
 (`!a n x y. (a + x == a + y) (mod n) ==> (x == y) (mod n)`,

  INTEGER_TAC);;


let INT_CONG_ADD_LCANCEL_EQ_0 = 
prove
 (`!a n x y. (a + x == a) (mod n) <=> (x == &0) (mod n)`,

  INTEGER_TAC);;


let INT_CONG_ADD_RCANCEL_EQ_0 = 
prove
 (`!a n x y. (x + a == a) (mod n) <=> (x == &0) (mod n)`,

  INTEGER_TAC);;


let INT_CONG_INT_DIVIDES_MODULUS = 
prove
 (`!x y m n. (x == y) (mod m) /\ n divides m ==> (x == y) (mod n)`,

  INTEGER_TAC);;


let INT_CONG_0_DIVIDES = 
prove
 (`!n x. (x == &0) (mod n) <=> n divides x`,

  INTEGER_TAC);;


let INT_CONG_1_DIVIDES = 
prove
 (`!n x. (x == &1) (mod n) ==> n divides (x - &1)`,

  INTEGER_TAC);;


let INT_CONG_DIVIDES = 
prove
 (`!x y n. (x == y) (mod n) ==> (n divides x <=> n divides y)`,

  INTEGER_TAC);;


let INT_CONG_COPRIME = 
prove
 (`!x y n. (x == y) (mod n) ==> (coprime(n,x) <=> coprime(n,y))`,

  INTEGER_TAC);;


let INT_CONG_MOD_MULT = 
prove
 (`!x y m n. (x == y) (mod n) /\ m divides n ==> (x == y) (mod m)`,

  INTEGER_TAC);;


let INT_CONG_TO_1 = 
prove
 (`!a n. (a == &1) (mod n) <=> ?m. a = &1 + m * n`,

  INTEGER_TAC);;


let INT_CONG_SOLVE = 
prove
 (`!a b n. coprime(a,n) ==> ?x. (a * x == b) (mod n)`,

  INTEGER_TAC);;


let INT_CONG_SOLVE_UNIQUE = 
prove
 (`!a b n. coprime(a,n)
           ==> !x y. (a * x == b) (mod n) /\ (a * y == b) (mod n)
                     ==> (x == y) (mod n)`,

  INTEGER_TAC);;


let INT_CONG_CHINESE = 
prove
 (`coprime(a,b) /\ (x == y) (mod a) /\ (x == y) (mod b)
   ==> (x == y) (mod (a * b))`,

  INTEGER_TAC);;


let INT_CHINESE_REMAINDER_COPRIME = 
prove
 (`!a b m n.
        coprime(a,b) /\ ~(a = &0) /\ ~(b = &0) /\ coprime(m,a) /\ coprime(n,b)
        ==> ?x. coprime(x,a * b) /\
                (x == m) (mod a) /\ (x == n) (mod b)`,

  INTEGER_TAC);;


let INT_CHINESE_REMAINDER_COPRIME_UNIQUE = 
prove
 (`!a b m n x y.
        coprime(a,b) /\
        (x == m) (mod a) /\ (x == n) (mod b) /\
        (y == m) (mod a) /\ (y == n) (mod b)
        ==> (x == y) (mod (a * b))`,

  INTEGER_TAC);;


let SOLVABLE_GCD = 
prove
 (`!a b n. gcd(a,n) divides b ==> ?x. (a * x == b) (mod n)`,

  INTEGER_TAC);;


let INT_LINEAR_CONG_POS = 
prove
 (`!n a x:int. ~(n = &0) ==> ?y. &0 <= y /\ (a * x == a * y) (mod n)`,

  REPEAT STRIP_TAC THEN EXISTS_TAC `x + abs(x * n):int` THEN CONJ_TAC THENL
   [MATCH_MP_TAC(INT_ARITH `abs(x:int) * &1 <= y ==> &0 <= x + y`) THEN
    REWRITE_TAC[INT_ABS_MUL] THEN MATCH_MP_TAC INT_LE_LMUL THEN
    ASM_INT_ARITH_TAC;
    MATCH_MP_TAC(INTEGER_RULE
     `n divides y ==> (a * x:int == a * (x + y)) (mod n)`) THEN
    REWRITE_TAC[INT_DIVIDES_RABS] THEN INTEGER_TAC]);;


let INT_CONG_SOLVE_POS = 
prove
 (`!a b n:int.
        coprime(a,n) /\ ~(n = &0 /\ abs a = &1)
        ==> ?x. &0 <= x /\ (a * x == b) (mod n)`,

  REPEAT GEN_TAC THEN ASM_CASES_TAC `n:int = &0` THEN
  ASM_REWRITE_TAC[INT_COPRIME_0; INT_DIVIDES_ONE] THENL
   [INT_ARITH_TAC;
    ASM_MESON_TAC[INT_LINEAR_CONG_POS; INT_CONG_SOLVE; INT_CONG_TRANS;
                  INT_CONG_SYM]]);;


let INT_CONG_IMP_EQ = 
prove
 (`!x y n:int. abs(x - y) < n /\ (x == y) (mod n) ==> x = y`,

  REPEAT GEN_TAC THEN
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  ONCE_REWRITE_TAC[int_congruent; GSYM INT_SUB_0] THEN
  DISCH_THEN(X_CHOOSE_THEN `q:int` SUBST_ALL_TAC) THEN
  FIRST_X_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
   `abs(n * q) < n ==> abs(n * q) < abs n * &1`)) THEN
  REWRITE_TAC[INT_ABS_MUL; INT_ENTIRE] THEN
  REWRITE_TAC[INT_ARITH
   `abs n * (q:int) < abs n * &1 <=> ~(&0 <= abs n * (q - &1))`] THEN
  ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[DE_MORGAN_THM] THEN
  STRIP_TAC THEN MATCH_MP_TAC INT_LE_MUL THEN ASM_INT_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* A stronger form of the CRT.                                               *)
(* ------------------------------------------------------------------------- *)


let INT_CRT_STRONG = 
prove
 (`!a1 a2 n1 n2:int.
        (a1 == a2) (mod (gcd(n1,n2)))
        ==> ?x. (x == a1) (mod n1) /\ (x == a2) (mod n2)`,

  INTEGER_TAC);;


let INT_CRT_STRONG_IFF = 
prove
 (`!a1 a2 n1 n2:int.
        (?x. (x == a1) (mod n1) /\ (x == a2) (mod n2)) <=>
        (a1 == a2) (mod (gcd(n1,n2)))`,

  INTEGER_TAC);;

(* ------------------------------------------------------------------------- *)
(* Other miscellaneous lemmas.                                               *)
(* ------------------------------------------------------------------------- *)


let EVEN_SQUARE_MOD4 = 
prove
 (`((&2 * n) pow 2 == &0) (mod &4)`,

  INTEGER_TAC);;


let ODD_SQUARE_MOD4 = 
prove
 (`((&2 * n + &1) pow 2 == &1) (mod &4)`,

  INTEGER_TAC);;


let INT_DIVIDES_LE = 
prove
 (`!x y. x divides y ==> abs(x) <= abs(y) \/ y = &0`,

  REWRITE_TAC[int_divides; LEFT_IMP_EXISTS_THM] THEN
  MAP_EVERY X_GEN_TAC [`x:int`; `y:int`; `z:int`] THEN
  DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[INT_ABS_MUL; INT_ENTIRE] THEN
  REWRITE_TAC[INT_ARITH `x <= x * z <=> &0 <= x * (z - &1)`] THEN
  ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[] THEN
  ASM_CASES_TAC `z = &0` THEN ASM_REWRITE_TAC[] THEN
  MATCH_MP_TAC INT_LE_MUL THEN ASM_INT_ARITH_TAC);;


let INT_DIVIDES_POW_LE = 
prove
 (`!p m n. &2 <= abs p ==> ((p pow m) divides (p pow n) <=> m <= n)`,

  REPEAT STRIP_TAC THEN EQ_TAC THENL
   [DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN
    ASM_SIMP_TAC[INT_POW_EQ_0; INT_ARITH `&2 <= abs p ==> ~(p = &0)`] THEN
    ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
    REWRITE_TAC[INT_NOT_LE; NOT_LE; INT_ABS_POW] THEN
    ASM_MESON_TAC[INT_POW_MONO_LT; ARITH_RULE `&2 <= x ==> &1 < x`];
    SIMP_TAC[LE_EXISTS; LEFT_IMP_EXISTS_THM; INT_POW_ADD] THEN INTEGER_TAC]);;

(* ------------------------------------------------------------------------- *)
(* Integer primality / irreducibility.                                       *)
(* ------------------------------------------------------------------------- *)


let int_prime = new_definition
 `int_prime p <=> abs(p) > &1 /\
                  !x. x divides p ==> abs(x) = &1 \/ abs(x) = abs(p)`;;


let INT_PRIME_NEG = 
prove
 (`!p. int_prime(--p) <=> int_prime p`,

  REWRITE_TAC[int_prime; INT_DIVIDES_RNEG; INT_ABS_NEG]);;


let INT_PRIME_ABS = 
prove
 (`!p. int_prime(abs p) <=> int_prime p`,

  GEN_TAC THEN REWRITE_TAC[INT_ABS] THEN
  COND_CASES_TAC THEN ASM_REWRITE_TAC[INT_PRIME_NEG]);;


let INT_PRIME_GE_2 = 
prove
 (`!p. int_prime p ==> &2 <= abs(p)`,

  REWRITE_TAC[int_prime] THEN INT_ARITH_TAC);;


let INT_PRIME_0 = 
prove
 (`~(int_prime(&0))`,

  REWRITE_TAC[int_prime] THEN INT_ARITH_TAC);;


let INT_PRIME_1 = 
prove
 (`~(int_prime(&1))`,

  REWRITE_TAC[int_prime] THEN INT_ARITH_TAC);;


let INT_PRIME_2 = 
prove
 (`int_prime(&2)`,

  REWRITE_TAC[int_prime] THEN CONV_TAC INT_REDUCE_CONV THEN
  X_GEN_TAC `x:int` THEN
  ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[INT_DIVIDES_ZERO] THEN
  CONV_TAC INT_REDUCE_CONV THEN
  DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC);;


let INT_PRIME_FACTOR = 
prove
 (`!x. ~(abs x = &1) ==> ?p. int_prime p /\ p divides x`,

  MATCH_MP_TAC WF_INT_MEASURE THEN EXISTS_TAC `abs` THEN
  REWRITE_TAC[INT_ABS_POS] THEN X_GEN_TAC `x:int` THEN
  REPEAT STRIP_TAC THEN ASM_CASES_TAC `int_prime x` THENL
   [EXISTS_TAC `x:int` THEN ASM_REWRITE_TAC[] THEN
    REPEAT(POP_ASSUM MP_TAC) THEN INTEGER_TAC;
    ALL_TAC] THEN
  ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[] THENL
   [EXISTS_TAC `&2` THEN ASM_REWRITE_TAC[INT_PRIME_2; INT_DIVIDES_0];
    ALL_TAC] THEN
  FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [int_prime]) THEN
  ASM_SIMP_TAC[INT_ARITH `~(x = &0) /\ ~(abs x = &1) ==> abs x > &1`] THEN
  REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; DE_MORGAN_THM] THEN
  DISCH_THEN(X_CHOOSE_THEN `y:int` STRIP_ASSUME_TAC) THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `y:int`) THEN ASM_REWRITE_TAC[] THEN
  ANTS_TAC THENL
   [FIRST_X_ASSUM(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC;
    MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN SIMP_TAC[] THEN
    UNDISCH_TAC `y divides x` THEN INTEGER_TAC]);;


let INT_PRIME_FACTOR_LT = 
prove
 (`!n m p. int_prime(p) /\ ~(n = &0) /\ n = p * m ==> abs m < abs n`,

  REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[INT_ABS_MUL] THEN
  MATCH_MP_TAC(INT_ARITH `&0 < m * (p - &1) ==> m < p * m`) THEN
  MATCH_MP_TAC INT_LT_MUL THEN
  UNDISCH_TAC `~(n = &0)` THEN ASM_CASES_TAC `m = &0` THEN
  ASM_REWRITE_TAC[INT_MUL_RZERO] THEN DISCH_THEN(K ALL_TAC) THEN
  CONJ_TAC THENL [ASM_INT_ARITH_TAC; ALL_TAC] THEN
  FIRST_ASSUM(MP_TAC o MATCH_MP INT_PRIME_GE_2) THEN INT_ARITH_TAC);;


let INT_PRIME_FACTOR_INDUCT = 
prove
 (`!P. P(&0) /\ P(&1) /\ P(-- &1) /\
       (!p n. int_prime p /\ ~(n = &0) /\ P n ==> P(p * n))
       ==> !n. P n`,

  GEN_TAC THEN STRIP_TAC THEN
  MATCH_MP_TAC WF_INT_MEASURE THEN EXISTS_TAC `abs` THEN
  REWRITE_TAC[INT_ABS_POS] THEN X_GEN_TAC `n:int` THEN DISCH_TAC THEN
  ASM_CASES_TAC `n = &0` THEN ASM_REWRITE_TAC[] THEN
  ASM_CASES_TAC `abs n = &1` THENL
   [ASM_MESON_TAC[INT_ARITH `abs x = &a <=> x = &a \/ x = -- &a`];
    ALL_TAC] THEN
  FIRST_ASSUM(X_CHOOSE_THEN `p:int`
    STRIP_ASSUME_TAC o MATCH_MP INT_PRIME_FACTOR) THEN
  FIRST_X_ASSUM(X_CHOOSE_THEN `d:int` SUBST_ALL_TAC o
    GEN_REWRITE_RULE I [int_divides]) THEN
  FIRST_X_ASSUM(MP_TAC o SPECL [`p:int`; `d:int`]) THEN
  RULE_ASSUM_TAC(REWRITE_RULE[INT_ENTIRE; DE_MORGAN_THM]) THEN
  DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
  FIRST_X_ASSUM MATCH_MP_TAC THEN
  ASM_MESON_TAC[INT_PRIME_FACTOR_LT; INT_ENTIRE]);;

(* ------------------------------------------------------------------------- *)
(* Infinitude.                                                               *)
(* ------------------------------------------------------------------------- *)


let INT_DIVIDES_FACT = 
prove
 (`!n x. &1 <= abs(x) /\ abs(x) <= &n ==> x divides &(FACT n)`,

  INDUCT_TAC THENL [INT_ARITH_TAC; ALL_TAC] THEN
  REWRITE_TAC[FACT; INT_ARITH `x <= &n <=> x = &n \/ x < &n`] THEN
  REWRITE_TAC[GSYM INT_OF_NUM_SUC; INT_ARITH `x < &m + &1 <=> x <= &m`] THEN
  REWRITE_TAC[INT_OF_NUM_SUC; GSYM INT_OF_NUM_MUL] THEN REPEAT STRIP_TAC THEN
  ASM_SIMP_TAC[INT_DIVIDES_LMUL] THEN
  MATCH_MP_TAC INT_DIVIDES_RMUL THEN
  ASM_MESON_TAC[INT_DIVIDES_LABS; INT_DIVIDES_REFL]);;


let INT_EUCLID_BOUND = 
prove
 (`!n. ?p. int_prime(p) /\ &n < p /\ p <= &(FACT n) + &1`,

  GEN_TAC THEN MP_TAC(SPEC `&(FACT n) + &1` INT_PRIME_FACTOR) THEN
  REWRITE_TAC[INT_OF_NUM_ADD; INT_ABS_NUM; INT_OF_NUM_EQ] THEN
  REWRITE_TAC[EQ_ADD_RCANCEL_0; FACT_NZ; GSYM INT_OF_NUM_ADD] THEN
  DISCH_THEN(X_CHOOSE_THEN `p:int` STRIP_ASSUME_TAC) THEN
  EXISTS_TAC `abs p` THEN ASM_REWRITE_TAC[INT_PRIME_ABS] THEN CONJ_TAC THENL
   [ALL_TAC;
    FIRST_ASSUM(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN
    REWRITE_TAC[GSYM INT_OF_NUM_ADD; GSYM INT_OF_NUM_SUC] THEN
    INT_ARITH_TAC] THEN
  REWRITE_TAC[GSYM INT_NOT_LE] THEN DISCH_TAC THEN
  MP_TAC(SPECL [`n:num`; `p:int`] INT_DIVIDES_FACT) THEN
  ASM_SIMP_TAC[INT_PRIME_GE_2; INT_ARITH `&2 <= p ==> &1 <= p`] THEN
  DISCH_TAC THEN SUBGOAL_THEN `p divides &1` MP_TAC THENL
   [REPEAT(POP_ASSUM MP_TAC) THEN INTEGER_TAC;
    REWRITE_TAC[INT_DIVIDES_ONE] THEN
    ASM_MESON_TAC[INT_PRIME_NEG; INT_PRIME_1]]);;


let INT_EUCLID = 
prove
 (`!n. ?p. int_prime(p) /\ p > n`,

  MP_TAC INT_IMAGE THEN MATCH_MP_TAC MONO_FORALL THEN
  X_GEN_TAC `n:int` THEN REWRITE_TAC[INT_GT] THEN
  ASM_REWRITE_TAC[OR_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
  MP_TAC INT_EUCLID_BOUND THEN MATCH_MP_TAC MONO_FORALL THEN
  X_GEN_TAC `m:num` THEN DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
  MATCH_MP_TAC MONO_EXISTS THEN SIMP_TAC[] THEN
  FIRST_X_ASSUM(DISJ_CASES_THEN SUBST1_TAC) THEN INT_ARITH_TAC);;


let INT_PRIMES_INFINITE = 
prove
 (`INFINITE {p | int_prime p}`,

  SUBGOAL_THEN `INFINITE {n | int_prime(&n)}` MP_TAC THEN
  REWRITE_TAC[INFINITE; CONTRAPOS_THM] THENL
   [REWRITE_TAC[num_FINITE; IN_ELIM_THM] THEN
    REWRITE_TAC[NOT_EXISTS_THM; NOT_FORALL_THM; NOT_IMP; NOT_LE] THEN
    REWRITE_TAC[GSYM INT_OF_NUM_LT; INT_EXISTS_POS] THEN
    MP_TAC INT_EUCLID_BOUND THEN
    MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN
    MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN
    SIMP_TAC[] THEN INT_ARITH_TAC;
    MP_TAC(ISPECL [`&`; `{p | int_prime p}`] FINITE_IMAGE_INJ) THEN
    REWRITE_TAC[INT_OF_NUM_EQ; IN_ELIM_THM]]);;


let INT_COPRIME_PRIME = 
prove
 (`!p a b. coprime(a,b) ==> ~(int_prime(p) /\ p divides a /\ p divides b)`,

  REWRITE_TAC[int_coprime] THEN
  MESON_TAC[INT_DIVIDES_ONE; INT_PRIME_NEG; INT_PRIME_1]);;


let INT_COPRIME_PRIME_EQ = 
prove
 (`!a b. coprime(a,b) <=> !p. ~(int_prime(p) /\ p divides a /\ p divides b)`,

  REPEAT GEN_TAC THEN EQ_TAC THENL [MESON_TAC[INT_COPRIME_PRIME]; ALL_TAC] THEN
  ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
  REWRITE_TAC[int_coprime; INT_DIVIDES_ONE_ABS] THEN
  ONCE_REWRITE_TAC[NOT_FORALL_THM] THEN REWRITE_TAC[NOT_IMP] THEN
  DISCH_THEN(X_CHOOSE_THEN `d:int` STRIP_ASSUME_TAC) THEN
  FIRST_ASSUM(X_CHOOSE_TAC `p:int` o MATCH_MP INT_PRIME_FACTOR) THEN
  EXISTS_TAC `p:int` THEN ASM_MESON_TAC[INT_DIVIDES_TRANS]);;


let INT_PRIME_COPRIME = 
prove
 (`!x p. int_prime(p) ==> p divides x \/ coprime(p,x)`,

  REPEAT STRIP_TAC THEN REWRITE_TAC[int_coprime] THEN
  MATCH_MP_TAC(TAUT `(~b ==> a) ==> a \/ b`) THEN
  REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; INT_DIVIDES_ONE_ABS] THEN
  DISCH_THEN(X_CHOOSE_THEN `d:int` STRIP_ASSUME_TAC) THEN
  FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [int_prime]) THEN
  DISCH_THEN(MP_TAC o SPEC `d:int` o CONJUNCT2) THEN ASM_REWRITE_TAC[] THEN
  ASM_MESON_TAC[INT_DIVIDES_TRANS; INT_DIVIDES_LABS; INT_DIVIDES_RABS]);;


let INT_PRIME_COPRIME_EQ = 
prove
 (`!p n. int_prime p ==> (coprime(p,n) <=> ~(p divides n))`,

  REPEAT STRIP_TAC THEN
  MATCH_MP_TAC(TAUT `(b \/ a) /\ ~(a /\ b) ==> (a <=> ~b)`) THEN
  ASM_SIMP_TAC[INT_PRIME_COPRIME; int_coprime; INT_DIVIDES_ONE_ABS] THEN
  ASM_MESON_TAC[INT_DIVIDES_REFL; INT_PRIME_1; INT_PRIME_ABS]);;


let INT_COPRIME_PRIMEPOW = 
prove
 (`!p k m. int_prime p /\ ~(k = 0)
           ==> (coprime(m,p pow k) <=> ~(p divides m))`,

  SIMP_TAC[INT_COPRIME_RPOW] THEN ONCE_REWRITE_TAC[INT_COPRIME_SYM] THEN
  SIMP_TAC[INT_PRIME_COPRIME_EQ]);;


let INT_COPRIME_BEZOUT = 
prove
 (`!a b. coprime(a,b) <=> ?x y. a * x + b * y = &1`,

  INTEGER_TAC);;


let INT_COPRIME_BEZOUT_ALT = 
prove
 (`!a b. coprime(a,b) ==> ?x y. a * x = b * y + &1`,

  INTEGER_TAC);;


let INT_BEZOUT_PRIME = 
prove
 (`!a p. int_prime p /\ ~(p divides a) ==> ?x y. a * x = p * y + &1`,


let INT_PRIME_DIVPROD = 
prove
 (`!p a b. int_prime(p) /\ p divides (a * b) ==> p divides a \/ p divides b`,

  ONCE_REWRITE_TAC[TAUT `a /\ b ==> c \/ d <=> a ==> (~c /\ ~d ==> ~b)`] THEN
  SIMP_TAC[GSYM INT_PRIME_COPRIME_EQ] THEN INTEGER_TAC);;


let INT_PRIME_DIVPROD_EQ = 
prove
 (`!p a b. int_prime(p)
           ==> (p divides (a * b) <=> p divides a \/ p divides b)`,

  MESON_TAC[INT_PRIME_DIVPROD; INT_DIVIDES_LMUL; INT_DIVIDES_RMUL]);;


let INT_PRIME_DIVPOW = 
prove
 (`!n p x. int_prime(p) /\ p divides (x pow n) ==> p divides x`,

  REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
  ASM_SIMP_TAC[GSYM INT_PRIME_COPRIME_EQ; INT_COPRIME_POW]);;


let INT_PRIME_DIVPOW_N = 
prove
 (`!n p x. int_prime p /\ p divides (x pow n) ==> (p pow n) divides (x pow n)`,


let INT_COPRIME_SOS = 
prove
 (`!x y. coprime(x,y) ==> coprime(x * y,x pow 2 + y pow 2)`,

  INTEGER_TAC);;


let INT_PRIME_IMP_NZ = 
prove
 (`!p. int_prime p ==> ~(p = &0)`,

  GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP INT_PRIME_GE_2) THEN
  INT_ARITH_TAC);;


let INT_DISTINCT_PRIME_COPRIME = 
prove
 (`!p q. int_prime p /\ int_prime q /\ ~(abs p = abs q) ==> coprime(p,q)`,

  REWRITE_TAC[GSYM INT_DIVIDES_ANTISYM_ABS] THEN
  MESON_TAC[INT_COPRIME_SYM; INT_PRIME_COPRIME_EQ]);;


let INT_PRIME_COPRIME_LT = 
prove
 (`!x p. int_prime p /\ &0 < abs x /\ abs x < abs p ==> coprime(x,p)`,

  ONCE_REWRITE_TAC[INT_COPRIME_SYM] THEN SIMP_TAC[INT_PRIME_COPRIME_EQ] THEN
  REPEAT GEN_TAC THEN STRIP_TAC THEN
  DISCH_THEN(MP_TAC o MATCH_MP INT_DIVIDES_LE) THEN ASM_INT_ARITH_TAC);;


let INT_DIVIDES_PRIME_PRIME = 
prove
 (`!p q. int_prime p /\ int_prime q  ==> (p divides q <=> abs p = abs q)`,

  REPEAT STRIP_TAC THEN EQ_TAC THENL
   [ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
    ASM_SIMP_TAC[GSYM INT_PRIME_COPRIME_EQ; INT_DISTINCT_PRIME_COPRIME];
    SIMP_TAC[GSYM INT_DIVIDES_ANTISYM_ABS]]);;


let INT_COPRIME_POW_DIVPROD = 
prove
 (`!d a b. (d pow n) divides (a * b) /\ coprime(d,a) ==> (d pow n) divides b`,


let INT_PRIME_COPRIME_CASES = 
prove
 (`!p a b. int_prime p /\ coprime(a,b) ==> coprime(p,a) \/ coprime(p,b)`,


let INT_PRIME_DIVPROD_POW = 
prove
 (`!n p a b. int_prime(p) /\ coprime(a,b) /\ (p pow n) divides (a * b)
             ==> (p pow n) divides a \/ (p pow n) divides b`,


let INT_DIVIDES_POW2_REV = 
prove
 (`!n a b. (a pow n) divides (b pow n) /\ ~(n = 0) ==> a divides b`,

  REPEAT GEN_TAC THEN ASM_CASES_TAC `gcd(a,b) = &0` THENL
   [ASM_MESON_TAC[INT_GCD_EQ_0; INT_DIVIDES_REFL]; ALL_TAC] THEN
  FIRST_ASSUM(MP_TAC o MATCH_MP INT_GCD_COPRIME_EXISTS) THEN
  STRIP_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
  ONCE_ASM_REWRITE_TAC[] THEN REWRITE_TAC[INT_POW_MUL] THEN
  ASM_SIMP_TAC[INT_POW_EQ_0; INT_DIVIDES_RMUL2_EQ] THEN
  DISCH_THEN(MP_TAC o MATCH_MP (INTEGER_RULE
   `a divides b ==> coprime(a,b) ==> a divides &1`)) THEN
  ASM_SIMP_TAC[INT_COPRIME_POW2] THEN
  ASM_MESON_TAC[INT_DIVIDES_POW2; INT_DIVIDES_TRANS; INT_DIVIDES_1]);;


let INT_DIVIDES_POW2_EQ = 
prove
 (`!n a b. ~(n = 0) ==> ((a pow n) divides (b pow n) <=> a divides b)`,


let INT_POW_MUL_EXISTS = 
prove
 (`!m n p k. ~(m = &0) /\ m pow k * n = p pow k ==> ?q. n = q pow k`,

  REPEAT GEN_TAC THEN ASM_CASES_TAC `k = 0` THEN
  ASM_SIMP_TAC[INT_POW; INT_MUL_LID] THEN STRIP_TAC THEN
  MP_TAC(SPECL [`k:num`; `m:int`; `p:int`] INT_DIVIDES_POW2_REV) THEN
  ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
   [ASM_MESON_TAC[int_divides; INT_MUL_SYM]; ALL_TAC] THEN
  REWRITE_TAC[int_divides] THEN DISCH_THEN(CHOOSE_THEN SUBST_ALL_TAC) THEN
  FIRST_X_ASSUM(MP_TAC o SYM) THEN
  ASM_SIMP_TAC[INT_POW_MUL; INT_EQ_MUL_LCANCEL; INT_POW_EQ_0] THEN
  MESON_TAC[]);;


let INT_COPRIME_POW_ABS = 
prove
 (`!n a b c. coprime(a,b) /\ a * b = c pow n
             ==> ?r s. abs a = r pow n /\ abs b = s pow n`,

  GEN_TAC THEN GEN_REWRITE_TAC BINDER_CONV [SWAP_FORALL_THM] THEN
  GEN_REWRITE_TAC I [SWAP_FORALL_THM] THEN ASM_CASES_TAC `n = 0` THENL
   [ASM_REWRITE_TAC[INT_POW] THEN MESON_TAC[INT_ABS_MUL_1; INT_ABS_NUM];
    ALL_TAC] THEN
  MATCH_MP_TAC INT_PRIME_FACTOR_INDUCT THEN REPEAT CONJ_TAC THENL
   [REPEAT GEN_TAC THEN ASM_REWRITE_TAC[INT_POW_ZERO; INT_ENTIRE] THEN
    DISCH_THEN(CONJUNCTS_THEN2 MP_TAC DISJ_CASES_TAC) THEN
    ASM_SIMP_TAC[INT_COPRIME_0; INT_DIVIDES_ONE_ABS; INT_ABS_NUM] THEN
    ASM_MESON_TAC[INT_POW_ONE; INT_POW_ZERO];
    REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o AP_TERM `abs:int->int`) THEN
    SIMP_TAC[INT_POW_ONE; INT_ABS_NUM; INT_ABS_MUL_1] THEN
    MESON_TAC[INT_POW_ONE];
    REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o AP_TERM `abs:int->int`) THEN
    SIMP_TAC[INT_POW_ONE; INT_ABS_POW; INT_ABS_NEG; INT_ABS_NUM;
             INT_ABS_MUL_1] THEN MESON_TAC[INT_POW_ONE];
    REWRITE_TAC[INT_POW_MUL] THEN REPEAT STRIP_TAC THEN
    SUBGOAL_THEN `p pow n divides a \/ p pow n divides b` MP_TAC THENL
     [ASM_MESON_TAC[INT_PRIME_DIVPROD_POW; int_divides]; ALL_TAC] THEN
    REWRITE_TAC[int_divides] THEN
    DISCH_THEN(DISJ_CASES_THEN(X_CHOOSE_THEN `d:int` SUBST_ALL_TAC)) THEN
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INT_COPRIME_SYM]) THEN
    ASM_SIMP_TAC[INT_COPRIME_RMUL; INT_COPRIME_LMUL;
                 INT_COPRIME_LPOW; INT_COPRIME_RPOW] THEN
    STRIP_TAC THENL
     [FIRST_X_ASSUM(MP_TAC o SPECL [`b:int`; `d:int`]);
      FIRST_X_ASSUM(MP_TAC o SPECL [`d:int`; `a:int`])] THEN
    ASM_REWRITE_TAC[] THEN
    (ANTS_TAC THENL
      [MATCH_MP_TAC(INT_RING `!p. ~(p = &0) /\ a * p = b * p ==> a = b`) THEN
       EXISTS_TAC `p pow n` THEN
       ASM_SIMP_TAC[INT_POW_EQ_0; INT_PRIME_IMP_NZ] THEN
       FIRST_X_ASSUM(MP_TAC o SYM) THEN CONV_TAC INT_RING;
       STRIP_TAC THEN
       ASM_REWRITE_TAC[INT_ABS_POW; GSYM INT_POW_MUL; INT_ABS_MUL] THEN
       MESON_TAC[]])]);;


let INT_COPRIME_POW_ODD = 
prove
 (`!n a b c. ODD n /\ coprime(a,b) /\ a * b = c pow n
             ==> ?r s. a = r pow n /\ b = s pow n`,

  REPEAT STRIP_TAC THEN
  MP_TAC(SPECL [`n:num`; `a:int`; `b:int`; `c:int`] INT_COPRIME_POW_ABS) THEN
  ASM_REWRITE_TAC[INT_ABS] THEN
  REWRITE_TAC[RIGHT_EXISTS_AND_THM; LEFT_EXISTS_AND_THM] THEN
  MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[INT_ABS] THEN
  ASM_MESON_TAC[INT_POW_NEG; INT_NEG_NEG; NOT_ODD]);;


let INT_DIVIDES_PRIME_POW_LE = 
prove
 (`!p q m n. int_prime p /\ int_prime q
             ==> ((p pow m) divides (q pow n) <=>
                  m = 0 \/ abs p = abs q /\ m <= n)`,

  REPEAT STRIP_TAC THEN ASM_CASES_TAC `m = 0` THEN
  ASM_REWRITE_TAC[INT_POW; INT_DIVIDES_1] THEN
  GEN_REWRITE_TAC LAND_CONV [GSYM INT_DIVIDES_LABS] THEN
  GEN_REWRITE_TAC LAND_CONV [GSYM INT_DIVIDES_RABS] THEN
  REWRITE_TAC[INT_ABS_POW] THEN EQ_TAC THENL
   [DISCH_TAC THEN MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`);
    ALL_TAC] THEN
  ASM_MESON_TAC[INT_DIVIDES_POW_LE; INT_PRIME_GE_2; INT_PRIME_DIVPOW;
      INT_ABS_ABS; INT_PRIME_ABS; INT_DIVIDES_POW2; INT_DIVIDES_PRIME_PRIME]);;


let INT_EQ_PRIME_POW_ABS = 
prove
 (`!p q m n. int_prime p /\ int_prime q
             ==> (abs p pow m = abs q pow n <=>
                  m = 0 /\ n = 0 \/ abs p = abs q /\ m = n)`,

  REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM INT_ABS_POW] THEN
  GEN_REWRITE_TAC LAND_CONV [GSYM INT_DIVIDES_ANTISYM_ABS] THEN
  ASM_SIMP_TAC[INT_DIVIDES_PRIME_POW_LE; INT_PRIME_ABS] THEN
  ASM_CASES_TAC `abs p = abs q` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC);;


let INT_EQ_PRIME_POW_POS = 
prove
 (`!p q m n. int_prime p /\ int_prime q /\ &0 <= p /\ &0 <= q
             ==> (p pow m = q pow n <=>
                  m = 0 /\ n = 0 \/ p = q /\ m = n)`,

  REPEAT STRIP_TAC THEN
  MP_TAC(SPECL [`p:int`; `q:int`; `m:num`; `n:num`] INT_EQ_PRIME_POW_ABS) THEN
  ASM_SIMP_TAC[INT_ABS]);;


let INT_DIVIDES_FACT_PRIME = 
prove
 (`!p. int_prime p ==> !n. p divides &(FACT n) <=> abs p <= &n`,

  GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN REWRITE_TAC[FACT] THENL
   [REWRITE_TAC[INT_ARITH `abs x <= &0 <=> x = &0`] THEN
    ASM_MESON_TAC[INT_DIVIDES_ONE; INT_PRIME_NEG; INT_PRIME_0; INT_PRIME_1];
    ASM_SIMP_TAC[INT_PRIME_DIVPROD_EQ; GSYM INT_OF_NUM_MUL] THEN
    REWRITE_TAC[GSYM INT_OF_NUM_SUC] THEN
    ASM_MESON_TAC[INT_DIVIDES_LE; INT_ARITH `x <= n ==> x <= n + &1`;
                  INT_DIVIDES_REFL; INT_DIVIDES_LABS;
                  INT_ARITH `p <= n + &1 ==> p <= n \/ p = n + &1`;
                  INT_ARITH `~(&n + &1 = &0)`;
                  INT_ARITH `abs(&n + &1) = &n + &1`]]);;