proposition: Lemma FM_fuscc_val n: fusc (FMc n) = fib n.
proof: Proof. move: n; apply: is_fib => // n. rewrite FM_cE FM_dE FM_cE FM_recE1 (addnC (FMd n)) - addnA addnn. by case: (odd n); rewrite !fusc_odd -?doubleS fusc_even // addnC. 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)