proposition: Lemma FM_rece n: FMe (n.+4) = FMe (n.+3) + (FMe n.+2).*2.
proof: Proof. rewrite FM_rece2 FM_rece2 /=. case: (odd n); rewrite /negb addn0 ?subn0 addn1. by rewrite doubleS doubleS ! succnK addSn addnn. move: (FM_ebound n); case (FMe n.+2); first by rewrite leqn0 expn_eq0 /=. by move => x _; rewrite !doubleS !succnK addSn !addnS addnn. 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)