2013-06-30から1日間の記事一覧
sqrtp:theory begin importing ints@primes, ints@gcd, reals@sqrt lem1:lemma forall(p:int): prime?(p) => (exists(n:posint): p = n * n) => False %|- lem1 : PROOF %|- (then (skeep*) %|- (spread (case "divides (n,p)") %|- ((then (expand "prime?"…