let
n
be
Nat
;
:: thesis:
(
n
>=
1 implies 2
<=
(
n
+
1
)
!
)
assume
n
>=
1 ;
:: thesis:
2
<=
(
n
+
1
)
!
then
n
+
1
>=
1
+
1
by
XREAL_1:7
;
then
1
<
(
n
+
1
)
!
by
ASYMPT_1:55
;
then
1
+
1
<=
(
n
+
1
)
!
by
NAT_1:13
;
hence
2
<=
(
n
+
1
)
!
;
:: thesis:
verum