proposition: Lemma FM_rece2 n: FMe n.+3 = (FMe n.+2 + (odd n.+2)).*2.-1.
proof: Proof. have sa: odd n.+2 + FMd n.+2 <= 3 * 2 ^ n. by rewrite addnC -FM_recE1 -FM_ecval leq_addr. rewrite /Fib_fusc_sym FM_recc2 !succnK expnS mulnCA subnS -mul2n -mulnBr mul2n. rewrite (FM_recE1 n.+2) addnK subnDA subnK //- (leq_add2r (FMd n.+2)). by rewrite subnK // (leq_trans _ sa) // leq_addl. 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)