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;