let a, b be odd Integer; :: thesis: max (((a + b) mod 4),((a - b) mod 4)) = 2
A1: ( (a + b) mod (2 * 2) is even & (a - b) mod (2 * 2) is even ) ;
( 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 max (((a + b) mod 4),((a - b) mod 4)) = 2 by A1, XXREAL_0:def 10, SDM; :: thesis: verum