proposition: Lemma FM_fusce_val n: fusc (FMe n.+2) = fib n.+2.
proof: Proof. move: (FM_cbound n); rewrite expn2S => sa. by rewrite - FM_fuscc_val - (fusc_palindrome sa (FM_ecval 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)