proposition: Lemma FM_dbound n : 2 ^ n <= FMd (n.+2) < 2^(n.+1).
proof: Proof. elim: n => // n /andP[]. rewrite - leq_double -ltn_Sdouble - mul2n - (mul2n (2^ _)) - !expnS. move => ha hb; rewrite FM_recd2 addnC; apply /andP; split. by apply: (leq_trans ha); case:odd. by apply: leq_trans hb; 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)