proposition: Lemma bin_of_natK : cancel bin_of_nat nat_of_bin.
proof: Proof. have sub2nn n : n.*2 - n = n by rewrite -addnn addKn. case=> //= n; rewrite -[n in RHS]sub2nn. by elim: n {2 4}n => // m IHm [|[|n]] //=; rewrite IHm // natTrecE sub2nn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring