let def0 = new_definition `f0 n = n EXP 2 + n + 1` ;;
let def1 = new_definition `prop1 n <=> ~((f0 n) MOD 5 = 0)` ;;
let def2 = new_definition `prop2 n <=> prop1 n /\ prop1 (SUC n) /\ prop1 (SUC (SUC n)) /\ prop1 (SUC (SUC (SUC n))) /\ prop1 (SUC (SUC (SUC (SUC n))))` ;;
let lem1 = prove
(`!n. f0 (SUC (SUC (SUC (SUC (SUC n))))) = f0 n + (2 * n + 6) * 5`,
REWRITE_TAC [def0] THEN ARITH_TAC);;
let lem2 = prove
(`!n:num. prop2 n`,
INDUCT_TAC THENL
[REWRITE_TAC [def0;def1;def2] THEN ARITH_TAC;
POP_ASSUM MP_TAC THEN REWRITE_TAC [def2] THEN
STRIP_TAC THEN UNDISCH_TAC `prop1 n` THEN
ASM_SIMP_TAC [def1;lem1;CONTRAPOS_THM] THEN
MESON_TAC [MOD_MULT_ADD; ADD_AC]]);;
let theorem_20130310 = MESON[lem2;def0;def1;def2]`!n. ~( (n EXP 2 + n + 1) MOD 5= 0)`;;
val theorem_20130310 : thm = |- !n. ~((n EXP 2 + n + 1) MOD 5 = 0)