2013-03-13から1日間の記事一覧
g `!s t a b. &0<=s /\ &0<=t /\ s+t= &1 /\ &0<=a /\ &0<=b /\ a<=b ==> !n. (s*a+t*b) pow n <= s*a pow n + t*b pow n` ;; e( REPEAT GEN_TAC THEN STRIP_TAC );; e( INDUCT_TAC );; e( ASM_REAL_ARITH_TAC );; e( REWRITE_TAC [pow] );; let lem1 = MESO…