proposition: Lemma nat_of_binK : cancel nat_of_bin bin_of_nat.
proof: Proof. case=> //=; elim=> //= p; case: (nat_of_pos p) => //= n [<-]. by rewrite natTrecE !addnS {2}addnn; elim: {1 3}n. by rewrite natTrecE addnS /= addnS {2}addnn; elim: {1 3}n. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring