2016-05-18から1日間の記事一覧
g `!n. 8 <= n ==> (?x y. n = 3 * x + 5 * y)` ;; e( INDUCT_TAC );; e( ARITH_TAC );; e( REWRITE_TAC [LE] THEN REPEAT STRIP_TAC );; e( EXISTS_TAC `1` THEN EXISTS_TAC `1` THEN ASM_ARITH_TAC );; e( FIRST_X_ASSUM (fun t -> FIRST_ASSUM (MP_TAC o …