Example (22.4)

　今回は，先の和にを掛けてになる項と残りの和に分割する補題です．

let lemma01 = MP
(SPECL[`\k. &2 pow xn / &k`;`1`;`2 EXP xn`;`n - 2 EXP xn`]SUM_ADD_SPLIT)
(prove(`1 <= 2 EXP xn + 1`,MP_TAC(MESON[TWO; ZERO_LESS_EXP]`0 < 2 EXP n`) THEN ARITH_TAC));;
let lemma02 = MP
(SPECL[`\k. &2 pow xn / &k`;`1`;`2 EXP xn`]SUM_CLAUSES_RIGHT)
(MESON[TWO; ZERO_LESS_EXP; LE_1]`0 < 2 EXP xn /\ 1 <= 2 EXP xn`);;
g`!n xn. 2 <= n /\ 1 <= xn /\ 2 EXP xn <= n ==> &2 pow xn * sum (1..n) (\k. &1 / &k) = sum (1..2 EXP xn - 1) (\k. &2 pow xn / &k) + &1 + sum (2 EXP xn + 1..n) (\k. &2 pow xn / &k)`;;
e(REPEAT STRIP_TAC THEN SIMP_TAC[GSYM SUM_LMUL; GSYM REAL_INV_1OVER; GSYM real_div]);;
e(MP_TAC (lemma01) THEN ASSUME_TAC(UNDISCH(ARITH_RULE`2 EXP xn <= n ==> 2 EXP xn + n - 2 EXP xn = n`)) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[]);;
e(MP_TAC lemma02 THEN ASM_SIMP_TAC[GSYM REAL_OF_NUM_POW; REAL_ARITH`~(&2 = &0)`; POW_NZ; REAL_DIV_REFL] THEN BETA_TAC THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[]);;
e(SIMP_TAC[REAL_ADD_AC]);;
let thm5 = top_thm();;