2013-08-13から1日間の記事一覧
g`!x. &0 <= x ==> !n. &1 + &n * x <= (&1 + x) pow n`;; e(GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC);; e REAL_ARITH_TAC;; e(SIMP_TAC[pow;REAL] THEN ASSUME_TAC(SPEC_ALL REAL_POS));; e(ASM_MESON_TAC[REAL_LE_ADD;REAL_POS;REAL_LE_LMUL;REAL_LE_MUL;…