let n be Nat; :: thesis: n <= n !
( n + 1 <= 3 or 3 <= n ) by INT_1:7;
then ( (n + 1) - 1 <= 3 - 1 or 3 <= n ) by XREAL_1:9;
then CCS: ( not not n = 0 & ... & not n = 2 or 3 <= n ) ;

per cases ( n = 0 or n = 1 or n = 2 or n >= 3 ) by CCS;

suppose n = 0 ; :: thesis: n <= n !

hence n <= n ! ; :: thesis: verum

end;

suppose n = 1 ; :: thesis: n <= n !

hence n <= n ! by NEWTON:13; :: thesis: verum

end;

suppose n = 2 ; :: thesis: n <= n !

hence n <= n ! by NEWTON:14; :: thesis: verum

end;

suppose n >= 3 ; :: thesis: n <= n !

hence n <= n ! by ASYMPT_1:59; :: thesis: verum

end;

end;