let n be Element of NAT ; :: thesis: ex m being Element of NAT st
( n = 4 * m or n = (4 * m) + 1 or n = (4 * m) + 2 or n = (4 * m) + 3 )
take n div 4 ; :: thesis: ( n = 4 * (n div 4) or n = (4 * (n div 4)) + 1 or n = (4 * (n div 4)) + 2 or n = (4 * (n div 4)) + 3 )
set o = n mod 4;
A1: ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 )

proof

n mod 4 < 3 + 1 by NAT_D:1;
then A2: n mod 4 <= 2 + 1 by NAT_1:13;

now :: thesis: ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 )

per cases ( n mod 4 <= 2 or n mod 4 = 2 + 1 ) by A2, NAT_1:8;

suppose A3: n mod 4 <= 2 ; :: thesis: ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 )

now :: thesis: ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 )

per cases ( n mod 4 <= 1 or n mod 4 = 1 + 1 ) by A3, NAT_1:8;

suppose A4: n mod 4 <= 1 ; :: thesis: ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 )

now :: thesis: ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 )

per cases ( n mod 4 <= 0 or n mod 4 = 0 + 1 ) by A4, NAT_1:8;

suppose n mod 4 <= 0 ; :: thesis: ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 )

hence ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) by NAT_1:2; :: thesis: verum

end;

suppose n mod 4 = 0 + 1 ; :: thesis: ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 )

hence ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) ; :: thesis: verum

end;

end;

end;

hence ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) ; :: thesis: verum

end;

suppose n mod 4 = 1 + 1 ; :: thesis: ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 )

hence ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) ; :: thesis: verum

end;

end;

end;

hence ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) ; :: thesis: verum

end;

suppose n mod 4 = 2 + 1 ; :: thesis: ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 )

hence ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) ; :: thesis: verum

end;

end;

end;

hence ( n mod 4 = 0 or n mod 4 = 1 or n mod 4 = 2 or n mod 4 = 3 ) ; :: thesis: verum

end;

n = (4 * (n div 4)) + (n mod 4) by NAT_D:2;
hence ( n = 4 * (n div 4) or n = (4 * (n div 4)) + 1 or n = (4 * (n div 4)) + 2 or n = (4 * (n div 4)) + 3 ) by A1; :: thesis: verum