proposition: Lemma bin_invertI n: bin_invert (bin_invert n) = n.
proof: Proof. case: n => //n; move:(log2_bnd n); rewrite /= leq_eqVlt => /andP[/orP]. case; first by move/eqP => <- _; rewrite !bin_invert_exp2n. move => sa sb; move:(bin_invert_p1 sa) => sc. have li := (log2_bin_invert n.+1). set p := 2 ^ (log2 n.+1).-1. have sd: p.*2 = 2 ^ log2 n.+1 by rewrite -expn2S - log2S_k. have ha: p <= n.+1 <= p.*2 by rewrite (ltnW sa) sd (ltnW sb). have:p <= bin_invert n.+1 <= p.*2. rewrite - (leq_add2l n.+1) - (leq_add2l n.+1 (bin_invert n.+1)). by rewrite sc mulSn mul2n leq_add2r addnC leq_add2l andbC. move /andP => [];rewrite leq_eqVlt => /orP; case. move/eqP => se _; move/eqP: sc; rewrite -se -/p mulSnr eqn_add2r => /eqP sf. by move: sb; rewrite log2S_k expnS -sf ltnn. rewrite /p -li => /bin_invert_p1; rewrite li - sc addnC => /eqP. by rewrite eqn_add2r => /eqP. 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)