proposition: Lemma bin_of_nat_expn2 m : bin_of_nat (expn 2 m.+1) = BinNat.N.mul 2%num (bin_of_nat (expn 2 m)).
proof: Proof. set x := BinNat.N.mul _ _. by rewrite -(nat_of_binK x) {}/x nat_of_mul_bin bin_of_natK expnS. Qed.
imports: mathcomp(all_ssreflect fingroup perm)