proposition: Lemma Fib_add3 n: natp n -> Fib (n +c \3c) = Fib n +c cdouble (Fib (csucc n)).
proof: Proof. move => nN. rewrite (csum_nS _ NS2) (Fib_add nN NS2) Fib3 Fib2. by rewrite (Nprod1r (NS_Fib nN)) cprodC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)