2015-08-18から1日間の記事一覧
g(`!n. 3 < n ==> 2 EXP n < FACT n`);; e(INDUCT_TAC);; e(ARITH_TAC);; e(SIMP_TAC[LT;EXP;FACT]);; e(STRIP_TAC);; e(POP_ASSUM (SUBST1_TAC o GSYM) THEN ARITH_TAC);; e(MATCH_MP_TAC LESS_MULT);; e(ASM_ARITH_TAC);; prove (`!n. 3 < n ==> 2 EXP n <…