for D being non square Nat
for a, b, c, d being Integer
for n being Nat st a + (b * (sqrt D)) = (c + (d * (sqrt D))) |^ n holds
a - (b * (sqrt D)) = (c - (d * (sqrt D))) |^ n