let
m
,
n
be
Nat
;
:: thesis:
m
<=
m
to_power
(
n
+
1
)
per
cases
(
m
=
0
or 1
<=
m
)
by
NAT_1:14
;
suppose
m
=
0
;
:: thesis:
m
<=
m
to_power
(
n
+
1
)
hence
m
<=
m
to_power
(
n
+
1
)
;
:: thesis:
verum
end;
suppose
A1
: 1
<=
m
;
:: thesis:
m
<=
m
to_power
(
n
+
1
)
1
<=
n
+
1
by
NAT_1:11
;
then
m
to_power
1
<=
m
to_power
(
n
+
1
)
by
A1
,
PRE_FF:8
;
hence
m
<=
m
to_power
(
n
+
1
)
by
NEWTON:5
;
:: thesis:
verum
end;
end;