theorem Th18: :: PELLS_EQ:18

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 )