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