proposition: Lemma FM_e_value n (a := 5*(2^n)): FMe n.+2 = if odd n then (a.-1) %/3 else (a.+1)%/3.
proof: Proof. rewrite /a/Fib_fusc_sym FM_c_value/= expnS expnS mulnA pow2_mod3'. case: (odd n); rewrite /negb mulnSr mulnSr mulnA (mulnDl 5 4). set q := ((2 ^ n).-2 %/ 3); set u := _ %/3; have ->: u = (4 * q + 3). by rewrite /u mulnSr mulnSr mulnCA - addnA -addnS -(mulnDr 3 _ 3) mulKn. rewrite subnDr addnC addnA addnK ! mulnSr. by rewrite mulnCA -addnA addnS addnS succnK -(mulnDr 3 _ 3) mulKn // addnC. rewrite (addnS _ 3) succnK mulnCA - mulnSr mulKn// addnS - addn1. rewrite -[X in _ - X] (addn1) subnDr addnC. rewrite addnA addnK mulnSr - addnS mulnCA addnC -(mulnDr 3 _ 2) 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)