proposition: Lemma fusc_podd n: fusc n.*2.-1 = fusc n.-1 + fusc n.
proof: Proof. by case: n => // n; rewrite doubleS /= fusc_odd. 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)