proposition: Lemma perm_eq_perm (pe : 'S_n) : perm_eq (enum 'I_n) [seq pe i | i <- enum 'I_n].
proof: Proof. apply uniq_perm. + by rewrite enum_uniq. + rewrite map_inj_in_uniq ?enum_uniq //. by move=> x1 x2 _ _; apply perm_inj. move=> i. rewrite mem_enum inE. symmetry. apply/mapP. exists (perm_inv pe i). by rewrite mem_enum inE. by rewrite permKV. Qed.
imports: mathcomp(all_ssreflect fingroup perm)