proposition: Lemma fusc_eq0 n: (fusc n == 0) = (n == 0).
proof: Proof. elim /fusc_ind: n => //. by move => n H; rewrite double_eq0 fusc_even. by move => n h1 h2; rewrite fusc_odd addn_eq0 h1 h2 andbF. 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)