prove (`!n. ~((n EXP 2 + n + 1) MOD 5 = 0)`, GEN_TAC THEN MP_TAC (MP(SPECL[`n:num`;`5`]DIVISION)(ARITH_RULE`~(5=0)`)) THEN STRIP_TAC THEN FIRST_X_ASSUM SUBST1_TAC THEN MAP_EVERY ABBREV_TAC [`q = n DIV 5`;`r = n MOD 5`] THEN SIMP_TAC [NUM_R…

let def0 = new_definition `f0 n = n EXP 2 + n + 1` ;; let def1 = new_definition `prop1 n <=> ~((f0 n) MOD 5 = 0)` ;; let lem0 = prove (`prop2 0`, SIMP_TAC[def0;def1;def2] THEN ARITH_TAC);; let lem1 = prove (`!n. f0 (SUC (SUC (SUC (SUC (SUC…

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))) /\ pro…