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) (\…

g`!n. &1 + &n + &n * (&n - &1) / &2 <= &2 pow n`;; e INDUCT_TAC;; e REAL_ARITH_TAC;; e(SIMP_TAC[pow;REAL]);; e(SUBGOAL_TAC""`&n <= &n * &n`[ALL_TAC]);; e(DISJ_CASES_TAC(SIMP_RULE[GSYM REAL_LE;GSYM REAL_INJ](ARITH_RULE`n = 0 \/ 1 <= n`)));;…