proposition: Lemma FM_ebound n: 2 ^ n <= FMe (n.+2) <= 2^(n.+1).
proof: Proof. move:(FM_cbound n). rewrite -(leq_add2r (FMe n.+2)) -(leq_add2r (FMe n.+2) (FMc n.+2)). by rewrite FM_ecval mulSn leq_add2l -expnS addnC leq_add2l andbC. 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)