proposition: Lemma FM_cbound n: 2 ^ n <= FMc (n.+2) <= 2^(n.+1).
proof: Proof. move: (FM_cdbound n.+2) => /andP [sa sb]. move /andP: (FM_dbound n) => [sc sd]. by rewrite (leq_trans sc sa) (leq_trans sb sd). 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)