2013-03-09から1日間の記事一覧
#use "Library/prime.ml" ;; g `!p. prime p ==> !n. (n EXP p == n) (mod p)` ;; e( REPEAT STRIP_TAC );; e( MP_TAC (UNDISCH(SPEC_ALL PRIME_COPRIME_STRONG)) THEN STRIP_TAC );; e( FIRST_ASSUM (ASSUME_TAC o (REWRITE_RULE [GSYM CONG_0] ) ) );; e( …