let
m
be
Element
of
NAT
;
:: thesis:
Fib
(
m
+
1
)
<>
0
per
cases
(
m
=
0
or
m
<>
0
)
;
suppose
m
=
0
;
:: thesis:
Fib
(
m
+
1
)
<>
0
hence
Fib
(
m
+
1
)
<>
0
by
PRE_FF:1
;
:: thesis:
verum
end;
suppose
m
<>
0
;
:: thesis:
Fib
(
m
+
1
)
<>
0
hence
Fib
(
m
+
1
)
<>
0
by
Lm3
,
NAT_1:3
;
:: thesis:
verum
end;
end;