theorem :: PELLS_EQ:15

for D being square Nat
for p being positive Element of [:INT,INT:] st D > 0 holds
not p is Pell's_solution of D