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`)));;
e(ASM_SIMP_TAC[REAL_MUL_RZERO;REAL_LE_REFL]);;
e(ASM_MESON_TAC[REAL_LE_LMUL;REAL_POS;REAL_MUL_RID]);;
e ASM_REAL_ARITH_TAC;;
tst6:lemma forall(n:nat): 1 + n + n * (n - 1) / 2 <= 2 ^ n
%|- tst6 : PROOF
%|- (spread (induct "n" 1)
%|- ((grind)
%|- (then (skeep*)
%|- (spread (case "j <= j * j")
%|- ((grind)
%|- (then (delete -1 2)
%|- (spread (case "j = 0 or 1 <= j")
%|- ((spread (split) ((grind) (then (mult-by -1 "j") (grind))))
%|- (grind)))))))))
%|- QED
