proposition: Lemma fusc_reverse n:fusc (base2rev n) = fusc n.
proof: Proof. by move: (fuscj_reverse n); rewrite fuscj_0 fuscj_val. 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)