proposition: Lemma Nto_natE x : BinNat.N.to_nat x = nat_of_bin x.
proof: Proof. case x => //=. elim => [ | | //] p Hp /=. by rewrite Pnat.Pos2Nat.inj_xI NatTrec.trecE Hp -mul2n. by rewrite Pnat.Pos2Nat.inj_xO NatTrec.trecE Hp -mul2n. Qed.
imports: mathcomp(all_ssreflect fingroup perm)