let n be Nat; :: thesis: ( 4 divides n or 4 divides n + 1 or 4 divides n + 2 or 4 divides n + 3 )
assume CC: ( not 4 divides n & not 4 divides n + 1 & not 4 divides n + 2 & not 4 divides n + 3 ) ; :: thesis: contradiction
consider k being Nat such that
C1: ( n = 4 * k or n = (4 * k) + 1 or n = (4 * k) + 2 or n = (4 * k) + 3 ) by NUMBER02:24;

per cases ( n = 4 * k or n = (4 * k) + 1 or n = (4 * k) + 2 or n = (4 * k) + 3 ) by C1;

suppose n = 4 * k ; :: thesis: contradiction

hence contradiction by CC; :: thesis: verum

end;

suppose c2: n = (4 * k) + 1 ; :: thesis: contradiction

4 divides 4 * (k + 1) ;
hence contradiction by c2, CC; :: thesis: verum

end;

suppose c2: n = (4 * k) + 2 ; :: thesis: contradiction

4 divides 4 * (k + 1) ;
hence contradiction by c2, CC; :: thesis: verum

end;

suppose c2: n = (4 * k) + 3 ; :: thesis: contradiction

4 divides 4 * (k + 1) ;
hence contradiction by c2, CC; :: thesis: verum

end;

end;