theorem Th16: :: PELLS_EQ:16

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