g`sum (0..2) (\k. &(binom (n,k))) = &(binom (n,0)) + &(binom (n,1)) + &(binom (n,2))`;;
e(SIMP_TAC[REAL_ADD_ASSOC;TWO;ONE;ARITH_RULE`0 <= SUC 0 /\ 0 <= SUC (SUC 0)`;SUM_CLAUSES_NUMSEG]);;
let lem01 = top_thm ();;
g`2 <= n ==> sum (0..2) (\k. &(binom (n,k))) <= sum (0..n) (\k. &(binom (n,k)))`;;
e(DISCH_THEN(ASSUME_TAC o (MATCH_MP(SIMP_RULE[ARITH](SPECL[`(\k. &(binom (n,k)))`;`0`;`2`]SUM_COMBINE_R)))));;
e(MP_TAC(SIMP_RULE[REAL_POS](SPECL[`3`;`n:num`;`(\k. &(binom (n,k)))`]SUM_POS_LE_NUMSEG)));;
e ASM_REAL_ARITH_TAC;;
let lem02 = top_thm ();;
let lem03 = SIMP_RULE[GSYM(SIMP_RULE[REAL_POW_ONE;REAL_MUL_RID;REAL_ARITH`&1 + &1 = &2`](SPECL[`n:num`;`&1`;`&1`]REAL_BINOMIAL_THEOREM));SIMP_RULE[SIMP_RULE[BINOM_1;REAL_ADD;ARITH_RULE`1 + 1 = 2`;REAL_ARITH`a/b*c=c*a/b`](SPECL[`n:num`;`1`]BINOM_BOTTOM_STEP_REAL);BINOM_1;CONJUNCT1 binom;]lem01]lem02;;
