let
n
be
odd
Nat
;
:: thesis:
( not
n
<=
4 or
n
=
1 or
n
=
3 )
assume
A1
:
n
<=
4 ;
:: thesis:
(
n
=
1 or
n
=
3 )
n
<>
2
*
2 ;
then
n
<
3
+
1
by
A1
,
XXREAL_0:1
;
then
A2
:
n
<=
3
by
NAT_1:13
;
per
cases
(
n
=
3 or
n
<
2
+
1 )
by
A2
,
XXREAL_0:1
;
suppose
n
=
3 ;
:: thesis:
(
n
=
1 or
n
=
3 )
hence
(
n
=
1 or
n
=
3 ) ;
:: thesis:
verum
end;
suppose
n
<
2
+
1 ;
:: thesis:
(
n
=
1 or
n
=
3 )
then
n
<=
2
by
NAT_1:13
;
hence
(
n
=
1 or
n
=
3 )
by
Th6
;
:: thesis:
verum
end;
end;