let m be 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;