let
n
be
even
Nat
;
:: thesis:
(
n
<=
1 implies
n
=
0
)
assume
A1
:
n
<=
1 ;
:: thesis:
n
=
0
n
<>
(
2
*
0
)
+
1 ;
then
n
<
0
+
1
by
A1
,
XXREAL_0:1
;
hence
n
=
0
by
NAT_1:13
;
:: thesis:
verum