proposition: Lemma FM_recc: [/\ FMc 0 = 0, FMc 1 = 1 & forall n, FMc (n.+2) = FMc (n.+1) + (FMc n).*2 ].
proof: Proof. by split => // n; rewrite FM_cE FM_dE FM_cE addSn doubleD addnC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)