let lem2pn = GSYM(SIMP_RULE[REAL_POW_ONE;REAL_MUL_RID;REAL_ARITH`&1 + &1 = &2`](SPECL[`n:num`;`&1`;`&1`]REAL_BINOMIAL_THEOREM));;
g`sum (0..m) (\k. &(binom (n,k))) <= sum (0..n) (\k. &(binom (n,k)))`;;
e(DISJ_CASES_TAC(ARITH_RULE`m <= n \/ n <= m:num`));;
e(FIRST_ASSUM(MP_TAC o (MATCH_MP(SIMP_RULE[LE_0](SPECL[`(\k. &(binom (n,k)))`;`0`]SUM_COMBINE_R)))));;
e(SUBGOAL_TAC""`&0 <= sum (m + 1..n) (\k. &(binom (n,k)))`[ALL_TAC]);;
e(MATCH_MP_TAC SUM_POS_LE_NUMSEG);;
e(SIMP_TAC[REAL_POS]);;
e ASM_REAL_ARITH_TAC;;
e(FIRST_ASSUM(MP_TAC o (MATCH_MP(SIMP_RULE[LE_0](SPECL[`(\k. &(binom (n,k)))`;`0`]SUM_COMBINE_R)))));;
e(SUBGOAL_TAC""`sum (n + 1..m) (\k. &(binom (n,k))) = &0`[ALL_TAC]);;
e(MATCH_MP_TAC SUM_EQ_0_NUMSEG);;
(*e(SIMP_TAC[ARITH_RULE`n + 1 <= i ==> n < i`;BINOM_LT]);;*)
e(MESON_TAC[ADD1;OR_LESS;BINOM_LT]);;
e ASM_REAL_ARITH_TAC;;
let theorem2pn = SIMP_RULE[lem2pn](top_thm());;
# val theorem2pn : thm = |- sum (0..m) (\k. &(binom (n,k))) <= &2 pow n
