let m, n be Nat; :: thesis: ( ( ( n mod 4 = 1 & m mod 4 = 3 ) or ( n mod 4 = 3 & m mod 4 = 1 ) ) implies (n * m) mod 4 = 3 )
assume ( ( n mod 4 = 1 & m mod 4 = 3 ) or ( n mod 4 = 3 & m mod 4 = 1 ) ) ; :: thesis: (n * m) mod 4 = 3

per cases then ( ( n mod 4 = 1 & m mod 4 = 3 ) or ( n mod 4 = 3 & m mod 4 = 1 ) ) ;

suppose A1: ( n mod 4 = 1 & m mod 4 = 3 ) ; :: thesis: (n * m) mod 4 = 3

then (n * m) mod 4 = (1 * m) mod 4 by RADIX_2:3;
hence (n * m) mod 4 = 3 by A1; :: thesis: verum

end;

suppose A2: ( n mod 4 = 3 & m mod 4 = 1 ) ; :: thesis: (n * m) mod 4 = 3

then (n * m) mod 4 = (1 * n) mod 4 by RADIX_2:3;
hence (n * m) mod 4 = 3 by A2; :: thesis: verum

end;

end;