for D being Nat
for p being Pell's_solution of D st not D is square holds
( p is positive iff (p `1) + ((p `2) * (sqrt D)) > 1 )