proposition: Lemma Fib_even n: natp n -> Fib (cdouble (csucc n)) = Fib (csucc n) *c (cdouble (Fib n) +c Fib (csucc n)).
proof: Proof. move => nN. rewrite (double_succ nN) cdoubleE - (csum_nS _ nN). rewrite (Fib_add nN (NS_succ nN)) cprodC - cprodDr (Fib_rec nN). by rewrite csumA - cdoubleE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)