proposition: Lemma fusc_bin_invert n:fusc (bin_invert n) = fusc n.
proof: Proof. case: n => //n; move:(log2_bnd n); rewrite /= leq_eqVlt => /andP[/orP]. case; first by move /eqP => -{3 4} <- _; rewrite bin_invert_exp2n. move => sa sb; move:(bin_invert_p1 sa); set u := bin_invert _ => sc. symmetry;apply:(fusc_palindrome (i:= (log2 n.+1).-1)) => //. by rewrite (ltnW sa) -expn2S - log2S_k (ltnW sb). 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)