theorem Th13: :: PELLS_EQ:13

for D being Nat st not D is square holds
ex k, a, b, c, d being Integer st
( 0 <> k & (a ^2) - (D * (b ^2)) = k & k = (c ^2) - (D * (d ^2)) & a,c are_congruent_mod k & b,d are_congruent_mod k & ( |.a.| <> |.c.| or |.b.| <> |.d.| ) )