proposition: Lemma Fib_odd n (square := fun a => a *c a): natp n -> Fib (csucc (cdouble n)) = square (Fib n) +c square (Fib (csucc n)).
proof: Proof. by move => nN; rewrite cdoubleE (Fib_add nN nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)