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;REAL_RING`&1+(m+ &1)*x=(&1+x)*(&1+m*x)-m*x*x`;REAL_ARITH`&0<=a==>b<=c==>b-a<=c`]);;
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;REAL_RING`&1+(m+ &1)*x=(&1+x)*(&1+m*x)-m*x*x`;REAL_LE_ADDR;REAL_LE_SUB_RADD;REAL_LE_TRANS]);;
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_PV9_TAC[REAL_LE_ADD;REAL_POS;REAL_LE_LMUL;REAL_LE_MUL;REAL_RING`&1+(m+ &1)*x=(&1+x)*(&1+m*x)-m*x*x`;REAL_LE_ADDR;REAL_LE_SUB_RADD;REAL_LE_TRANS]);;
