proposition: Lemma FM_ecval n: FMc n.+2 + FMe n.+2 = 3 * 2 ^ n.
proof: Proof. case/andP: (FM_cbound n) => [le1 le2]. rewrite /Fib_fusc_sym succnK succnK mulSn -expnS -(addnBA (2 ^ n) le2). by rewrite - addnCA (addnC (FMc n.+2)) (subnK le2). 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)