let n be square Nat; :: thesis: for p being positive Element of [:INT,INT:] st n > 0 holds
not p is Pell's_solution of n
consider m being Nat such that
A1: n = m ^2 by PYTHTRIP:def 3;
let p be positive Element of [:INT,INT:]; :: thesis: ( n > 0 implies not p is Pell's_solution of n )
set p1 = p `1 ;
set p2 = p `2 ;
assume A2: ( n > 0 & p is Pell's_solution of n ) ; :: thesis: contradiction
then ((p `1) ^2) - (n * ((p `2) ^2)) = 1 by Def1;
then A3: ((p `1) - (m * (p `2))) * ((p `1) + (m * (p `2))) = 1 by A1;

per cases ( ( (p `1) - (m * (p `2)) = 1 & (p `1) + (m * (p `2)) = 1 ) or ( (p `1) - (m * (p `2)) = - 1 & (p `1) + (m * (p `2)) = - 1 ) ) by A3, INT_1:9;

suppose A4: ( (p `1) - (m * (p `2)) = 1 & (p `1) + (m * (p `2)) = 1 ) ; :: thesis: contradiction

m * (p `2) >= 1 * m by NAT_1:14, XREAL_1:64;
hence contradiction by A4, A1, A2; :: thesis: verum

end;

suppose ( (p `1) - (m * (p `2)) = - 1 & (p `1) + (m * (p `2)) = - 1 ) ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

end;