proposition: Lemma FM_d_val n: FMd n.+2 = zero_one_rep n.
proof: Proof. elim: n => //n Hrec; rewrite FM_recd2 Hrec /= addnC. rewrite {2} /zero_one_rep /= -/(zero_one_rep _). set h := head _ _;suff: h = ~~ odd n by move => <-; case: h. by rewrite /h {Hrec h}; elim: n => // n /= ->. 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)