theorem :: NEWTON06:54

for a, b being odd Nat holds (((a - b) / 2) |^ 2) mod (a * b) = (((a + b) / 2) |^ 2) mod (a * b)