proposition: Lemma bin_of_nat_inj : forall a b, bin_of_nat a = bin_of_nat b -> a = b.
proof: Proof. move=> a b X. have : nat_of_bin (bin_of_nat a) = nat_of_bin (bin_of_nat b) by rewrite X. by rewrite 2!bin_of_natK. Qed.
imports: mathcomp(all_ssreflect fingroup perm)