proposition: Lemma invsetK : cancel invset perm_of_invset.
proof: Proof. rewrite /perm_of_invset=> s; apply invg_inj; rewrite invgK. apply/permP => /= i; rewrite permE. have -> : s^-1 i = nth i [seq s^-1 i | i : 'I_n] i. by rewrite (nth_map i) ?size_enum_ord // nth_ord_enum. congr nth => {i}. apply (sorted_eq (@rsym_invset_trans s) (@rsym_invset_anti s)). - exact: (sort_sorted (@rsym_invset_total s)). - exact: rsym_invsetP. - rewrite perm_sort; apply uniq_perm. + exact: enum_uniq. + rewrite map_inj_uniq; first exact: enum_uniq. exact: perm_inj. + move=> /= i; apply esym. rewrite mem_enum inE; apply/mapP; exists (s i); first by rewrite mem_enum. by rewrite permK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr