theorem :: PELLS_EQ:21

for D being non square Nat
for p being Element of [:INT,INT:] holds
( p is positive Pell's_solution of D iff ex n being positive Nat st (p `1) + ((p `2) * (sqrt D)) = (((min_Pell's_solution_of D) `1) + (((min_Pell's_solution_of D) `2) * (sqrt D))) |^ n )