for D being Nat st not D is square holds
ex p being Pell's_solution of D st p is positive