let a, b be odd Integer; :: thesis: min (((a + b) mod 4),((a - b) mod 4)) = 0
( not not (a + b) mod (3 + 1) = 0 & ... & not (a + b) mod (3 + 1) = 3 & not not (a - b) mod (3 + 1) = 0 & ... & not (a - b) mod (3 + 1) = 3 ) by NUMBER03:11;
hence min (((a + b) mod 4),((a - b) mod 4)) = 0 by SDO; :: thesis: verum