Example (22.8)

　以上を利用して次に至ります．

g`~(?n N. 2 <= n /\ sum(1..n)(\k. &1 / &k) = &N)`;;
e(REPEAT STRIP_TAC);;
e(MP_TAC (SPEC_ALL floor2) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;
e(MP_TAC (SPEC`xn:num`thm4) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;
e(MP_TAC (SPEC_ALL thm5) THEN ASM_SIMP_TAC[]);;
e(MAP_EVERY (MP_TAC o SPEC_ALL) [thm7; thm8] THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN STRIP_TAC THEN ASM_SIMP_TAC[]);;
e(MP_TAC (SPECL[`x:num`;`y:num`;`x':num`;`y':num`]thm6) THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN ASM_SIMP_TAC[REAL_ARITH`&x' / &y' + &1 + &x / &y = &1 + &x / &y + &x' / &y'`; REAL_OF_NUM_POW; REAL_MUL]);;
let lemma = prove(`ODD y'' ==> (&(2 * m) = &1 + &x'' / &y'' <=> 2 * m * y'' = x'' + y'')`,STRIP_TAC THEN MP_TAC(UNDISCH(SPEC`y'':num`lemma01)) THEN SIMP_TAC[GSYM REAL_INJ; GSYM REAL_MUL; GSYM REAL_ADD;] THEN (CONV_TAC REAL_SOSFIELD));;
e(MP_TAC (MESON[ARITH_RULE`EVEN(2)`; LE_1; EVEN_EXP; EVEN_MULT]`1 <= xn ==> EVEN (2 EXP xn * N)`) THEN ASM_SIMP_TAC[EVEN_EXISTS] THEN STRIP_TAC THEN ASM_SIMP_TAC[UNDISCH lemma]);;
e(ASM_MESON_TAC[ARITH_RULE`EVEN 2`; EVEN_MULT; EVEN_ADD; EVEN_AND_ODD]);;

　更にintegerを用いて

MESON[top_thm(); integer; ABS_REFL; ARITH_RULE`1 <= x ==> 0 <= x`; REAL_LE; 
      REAL_LE_INV; SUM_POS_LE_NUMSEG; REAL_INV_1OVER]
`!n. 2 <= n ==> ~(integer (sum (1..n) (\k. &1 / &k)))`;;

となります．