proposition: Lemma perm_filter_enum_ord j : perm_eq [seq i <- enum 'I_n.+1 | i != j] [seq lift j i | i <- enum 'I_n].
proof: Proof. apply uniq_perm. + by rewrite filter_uniq // enum_uniq. + rewrite map_inj_in_uniq ?enum_uniq //. by move=> x1 x2 _ _; apply lift_inj. move=> k. rewrite mem_filter mem_enum andbT. symmetry. case: (unliftP j k) => /= [a|] ->. rewrite eq_sym neq_lift. rewrite mem_map. by rewrite mem_enum inE. by apply: lift_inj. rewrite eqxx. apply/mapP => /= -[x Hx]. move/(f_equal (@nat_of_ord _)). by apply/eqP/neq_lift. Qed.
imports: mathcomp(all_ssreflect fingroup perm)