proposition: Lemma FM_recE1 n: FMc n = (FMd n) + (odd n).
proof: Proof. elim: n => // n; rewrite FM_dE FM_cE /= => ->. by rewrite (addnAC _ (odd n)) addnn - addnA addnC; case: odd. 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)