theorem Th4: :: PELLS_EQ:4

for D, c, d, n being Nat ex a, b being Nat st a + (b * (sqrt D)) = (c + (d * (sqrt D))) |^ n