Example (22.3)

　今回は，先の和の各項の分母の中での指数がに等しいものは唯一つであり，その他のの指数はより小さいことの証明です．

g`!x y n. ODD y /\ 2 EXP x * y < 2 EXP (SUC n) ==> x <= n`;;
e(REPEAT STRIP_TAC);;
e(ASSUME_TAC(UNDISCH(MESON[ODD_EXISTS; LT_0; LE_1]`ODD y ==> 1 <= y`)));;
e(ASSUME_TAC(MESON[ZERO_LESS_EXP; TWO]`0 < 2 EXP x`));;
e(MP_TAC(SOS_RULE`2 EXP x * y < 2 EXP SUC n /\ 1 <= y /\ 0 < 2 EXP x==> 2 EXP x < 2 EXP SUC n`) THEN ASM_SIMP_TAC[GSYM LT_SUC_LE]);;
e(MESON_TAC[LE_REFL; NOT_SUC; TWO; LT_EXP]);;
let thm1 = top_thm();;

g`!x y n. ODD y /\ 2 EXP x * y < 2 EXP (SUC n) /\ x = n ==> y = 1`;;
e(REPEAT STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN FIRST_X_ASSUM MP_TAC);;
e(SIMP_TAC[EXP] THEN STRIP_TAC);;
e(ASSUME_TAC(MESON[ZERO_LESS_EXP; TWO]`0 < 2 EXP n`));;
e(MAP_EVERY MP_TAC[
MESON[ODD]`ODD y ==> ~(y = 0)`;
SPEC`2 EXP n`(SOS_RULE`!p. 0<p /\ p*y<2*p ==> y<2`)] THEN ASM_SIMP_TAC[]);;
e(ARITH_TAC);;
let thm2 = top_thm();;

g`!x y n. ODD y /\ 2 EXP x * y < 2 EXP (SUC n) ==> x = n /\ y = 1 \/ x < n`;;
e(REPEAT STRIP_TAC);;
e(MAP_EVERY(MP_TAC o SPEC_ALL)[thm2; thm1] THEN ASM_SIMP_TAC[]);;
e(ARITH_TAC);;
let thm3 = top_thm();;

g`!n k. 1 <= k /\ k < 2 EXP (SUC n) ==> (k = 2 EXP n \/ ( ~(k = 2 EXP n) /\ ?x y. k = 2 EXP x * y /\ x < n /\ ODD y))`;;
e(REPEAT STRIP_TAC);;
e(MP_TAC(SPEC`k:num`base2) THEN ASM_SIMP_TAC[LE_1] THEN REPEAT STRIP_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC);;
e(MP_TAC(SPEC_ALL thm3) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC);;
e(ASM_SIMP_TAC[MULT_CLAUSES]);;
e(ASM_MESON_TAC[]);;
let thm4 = top_thm();;