有理整数の性質 by HOL4.

やはり METIS は優秀です．
http://www.gilith.com/research/metis/
MESON による PROVE_TAC ではこうは行きません．

load "numRingLib";
open arithmeticTheory numLib numRingLib;

val def1 = Define `p n = (n*n+n+1) MOD 5 <> 0`;
val def2 = Define `p04 <=> (p 0)/\(p 1)/\(p 2)/\(p 3)/\(p 4)`;
val lem1 = ARITH_CONV``0<5:num``;
val lem2 = REDUCE_RULE(REWRITE_CONV[def1,def2]``p04``);

g `!n. (n * n + n + 1) MOD 5 <> 0` ;
e GEN_TAC;
e( SUBGOAL_THEN ``(n MOD 5 * n MOD 5 + n MOD 5 + 1) MOD 5 <> 0`` MP_TAC );
e( MP_TAC(PROVE[lem1,MOD_LESS]``(n MOD 5)< 5``) );
e( Q.ABBREV_TAC `r=n MOD 5` );;
e( METIS_TAC[def1,def2,lem2,ARITH_CONV``!r:num. (r<5)==>((r=0)\/(r=1)\/(r=2)\/(r=3)\/(r=4))``] );
e( METIS_TAC[lem1,MOD_MOD,MOD_PLUS,MOD_TIMES2] );

> val it =
    Proof manager status: 1 proof.
    1. Incomplete goalstack:
         Initial goal:
    
         ∀n. (n * n + n + 1) MOD 5 ≠ 0
    
    
     : proofs
- OK..
1 subgoal:
> val it =
    
    (n * n + n + 1) MOD 5 ≠ 0
    
     : proof
- OK..
2 subgoals:
> val it =
    
    (n MOD 5 * n MOD 5 + n MOD 5 + 1) MOD 5 ≠ 0 ⇒ (n * n + n + 1) MOD 5 ≠ 0
    
    
    
    (n MOD 5 * n MOD 5 + n MOD 5 + 1) MOD 5 ≠ 0
    
     : proof
- Meson search level: ...
OK..
1 subgoal:
> val it =
    
    n MOD 5 < 5 ⇒ (n MOD 5 * n MOD 5 + n MOD 5 + 1) MOD 5 ≠ 0
    
     : proof
- OK..
1 subgoal:
> val it =
    
    r < 5 ⇒ (r * r + r + 1) MOD 5 ≠ 0
    ------------------------------------
      Abbrev (r = n MOD 5)
     : proof
- - OK..
metis: r[+0+13]+0+0+0+0+0+0+0+0+0+0+0+5+0+0+0+0+0+1+4+1+4+1+4+1+10+3#

Goal proved.
 [Abbrev (r = n MOD 5)] |- r < 5 ⇒ (r * r + r + 1) MOD 5 ≠ 0

Goal proved.
 [] |- n MOD 5 < 5 ⇒ (n MOD 5 * n MOD 5 + n MOD 5 + 1) MOD 5 ≠ 0

Goal proved.
 [] |- (n MOD 5 * n MOD 5 + n MOD 5 + 1) MOD 5 ≠ 0

Remaining subgoals:
> val it =
    
    (n MOD 5 * n MOD 5 + n MOD 5 + 1) MOD 5 ≠ 0 ⇒ (n * n + n + 1) MOD 5 ≠ 0
    
     : proof
- OK..
metis: r[+0+7]+0+0+0+0+1+1+1+1+0+8+1+11+2+5+7+8+11+0+10+6+5+15+8+18r+7+9+22+18+22r+26+28+19+23r+13+10+31+30r+29+33+30+35r+35+34+55r#

Goal proved.
 []
|- (n MOD 5 * n MOD 5 + n MOD 5 + 1) MOD 5 ≠ 0 ⇒
   (n * n + n + 1) MOD 5 ≠ 0

Goal proved.
 [] |- (n * n + n + 1) MOD 5 ≠ 0
> val it =
    Initial goal proved.
     [] |- ∀n. (n * n + n + 1) MOD 5 ≠ 0
     : proof