proposition: Lemma FM_c_value n: FMc n = if odd n then ((2^n).+1) %/3 else ((2^n).-1)%/3.
proof: Proof. elim: n => //n; rewrite FM_recc2 expnS pow2_mod3'=> -> /=; case (odd n). rewrite /negb mulnSr mulnSr mulnCA -addnA (addnS _ 3) subn1 succnK mul2n. rewrite -addn3 -mulnSr -mulnSr !mulKn //. rewrite /= subn0 mulnSr mulnCA - addnS mul2n -mulnSr !mulKn //. 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)