let a, b be odd Nat; :: thesis: (((a - b) / 2) |^ 2) mod (a * b) = (((a + b) / 2) |^ 2) mod (a * b)
A1: ( ((a - b) / 2) |^ 2 = ((a - b) / 2) * ((a - b) / 2) & ((a + b) / 2) |^ 2 = ((a + b) / 2) * ((a + b) / 2) ) by NEWTON:81;
((((a - b) / 2) |^ 2) + (a * b)) mod (a * b) = (((((a - b) / 2) |^ 2) mod (a * b)) + ((a * b) mod (a * b))) mod (a * b) by NAT_D:66;
hence (((a - b) / 2) |^ 2) mod (a * b) = (((a + b) / 2) |^ 2) mod (a * b) by A1; :: thesis: verum