proposition: Lemma NS_Fib n: natp n -> natp (Fib n).
proof: Proof. move => nN; suff: natp (Fib n) /\ natp (Fib (csucc n)) by case. move: n nN; apply: Nat_induction. rewrite succ_zero Fib0 Fib1; fprops. move => n nN [sa sb]; split => //; rewrite (Fib_rec nN); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)