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 ;
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 ;
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 ;
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