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?" -2) (flatten) (inst -2 "n") (assert)
%|- (flatten) (replace -2 -4 LR) (cancel-by -4 "p"))
%|- (then (expand "divides") (inst?)))))
%|- QED
lem2:lemma forall(p:int,n,d:posint): rel_prime (n,d) => n * n = p * d * d => d = 1
%|- lem2 : PROOF
%|- (then (skeep*) (use "rel_prime_lem") (assert) (skeep*)
%|- (spread (case "1=m*m*(n*n)+2*m*n*n_1*d+n_1*n_1*d*d")
%|- ((then (replace -4 -1 LR)
%|- (spread (case "1=(m*m*d*p+2*m*n*n_1+n_1*n_1*d)*d")
%|- ((then (use "product_one") (assert)) (grind))))
%|- (grind))))
%|- QED
lem3:lemma forall(p:int): prime?(p) =>
(exists(n,d:posint): n / d = sqrt(p) & rel_prime (n,d)) => False
%|- lem3 : PROOF
%|- (then (skeep*) (mult-by -2 "d") (field -1)
%|- (spread (case "n * n = p * d * d")
%|- ((then (use* "lem2") (simplify -1) (replace -5 * LR)
%|- (replace -1 -2 LR) (simplify -2) (use* "lem1") (assert) (inst?)
%|- (grind))
%|- (grind))))
%|- QED
end sqrtp
