theorem :: NEWTON06:53

for a, b being non zero Nat holds ((a - b) |^ 2) mod ((4 * a) * b) = ((a + b) |^ 2) mod ((4 * a) * b)