#use "Library/prime.ml" ;;
g `!p. prime p ==> !n. (n EXP p == n) (mod p)` ;;
e( REPEAT STRIP_TAC );;
e( MP_TAC (UNDISCH(SPEC_ALL PRIME_COPRIME_STRONG)) THEN STRIP_TAC );;
e( FIRST_ASSUM (ASSUME_TAC o (REWRITE_RULE [GSYM CONG_0] ) ) );;
e( ASSUME_TAC (UNDISCH (SPECL[`p:num`;`p:num`;`n:num`;`0`]CONG_EXP)) );;
e( SUBST_ALL_TAC (UNDISCH(MESON[PRIME_GE_2;ARITH_RULE`2<=p==> ~(p=0)`;EXP_ZERO]`prime p ==> 0 EXP p =0`)) );;
e( ASM_MESON_TAC [CONG_SYM; CONG_TRANS] );;
let lem =UNDISCH_ALL(REWRITE_RULE[GSYM IMP_IMP](SPECL[`n:num`;`p:num`](ONCE_REWRITE_RULE[COPRIME_SYM]FERMAT_LITTLE_PRIME)));;
e( ASSUME_TAC lem );;
let lem = MESON[EXP_ADD;EXP_1;PRIME_GE_2;ARITH_RULE`2<=p==>1+p-1=p`]`prime p ==> n * n EXP (p-1) = n EXP p`;;
let lem = UNDISCH_ALL(MESON[SPECL[`n:num`;`p:num`]CONG_REFL;CONG_MULT;MULT_CLAUSES;lem]`(n EXP (p - 1) == 1) (mod p)==> prime p ==> (n EXP p == n) (mod p)`);;
e( ASM_SIMP_TAC [lem] );;
let lem = top_thm () ;;
let lem5 = MP(SPEC`5`lem)(EQT_ELIM(PRIME_TEST`5`));;
g `!n. ~( ( n EXP 2 + n + 1 == 0) (mod 5) )` ;;
e( REPEAT STRIP_TAC );;
let lem1 = MESON[LE_EXP;ARITH_RULE`1<=5/\ n=n EXP 1 /\ ~(1=0)`;]`!n. n <= n EXP 5`;;
let lem = MESON[CONG_SUB_CASES;lem1;CONG_SYM]`(n EXP 5 == n) (mod 5) <=> (n EXP 5 - n ==0) (mod 5)`;;
let lem = REWRITE_RULE [lem] lem5;;
e( ASSUME_TAC (SPEC_ALL lem) );;
e(MP_TAC(UNDISCH_ALL(SPECL[`(2 + 4 * n) `;` (n EXP 5 - n)`;`(1 + n + 2 * n EXP 2 + 2 * n EXP 3 + n EXP 4) `;` (n EXP 2+n+1)`;`5`](MESON[CONG_MULT;CONG_ADD;CONG_REFL; ARITH_RULE`x*0=0 /\ 0+0=0`]`!x m y n p. (m ==0) (mod p) ==> (n==0) (mod p) ==> (x*m+y*n==0) (mod p) `)) ));;
e( SIMP_TAC [ MP(SOS_RULE`n <= n EXP 5==>(2 + 4 * n) * (n EXP 5 - n)+(1 + n + 2 * n EXP 2 + 2 * n EXP 3 + n EXP 4) * (n EXP 2+n+1) = 1 + 5 * (n EXP 3 + n EXP 4 + n EXP 5 + n EXP 6)`)(SPEC_ALL lem1) ]);;
let lem = MESON[DIVIDES_REFL; CONG_0; CONG_MULT; CONG_REFL;MULT_CLAUSES]`!p x. (p*x==0) (mod p)`;;
e( REWRITE_TAC [MESON[lem; CONG_ADD; ADD_CLAUSES;CONG_SUB;ARITH_RULE`p*x<=1+p*x /\ 0<=0 /\ (1+p*x)-p*x=1/\ 0-0=0`]`!p x. (1+p*x==0) (mod p) <=> (1==0) (mod p)`] );;
e( MESON_TAC [CONG_0; DIVIDES_ONE; ARITH_RULE `~(5=1)` ] );;
let theorem_20130309 = top_thm () ;;
val theorem_20130309 : thm = |- !n. ~(n EXP 2 + n + 1 == 0) (mod 5)
