let
n
,
m
be
odd
Integer
;
:: thesis:
(
m
<
n
implies
m
+
2
<=
n
)
assume
m
<
n
;
:: thesis:
m
+
2
<=
n
then
m
+
1
<=
n
by
INT_1:7
;
then
m
+
1
<
n
by
XXREAL_0:1
;
then
(
m
+
1)
+
1
<=
n
by
INT_1:7
;
hence
m
+
2
<=
n
;
:: thesis:
verum