proposition: Lemma Fib_gt0 n: natp n -> n <> \0c -> (Fib n) <> \0c.
proof: Proof. move => nN nz; move:(cpred_pr nN nz) => [sa ->]. move: (cpred n) sa; clear n nN nz; apply: Nat_induction. rewrite succ_zero Fib1; fprops. by move => n nN Hr; rewrite (Fib_rec nN); move/csum_nz => [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)