proposition: Lemma perm_sort_inP (T : eqType) (leT : rel T) (s1 s2 : seq T) : {in s1 &, total leT} -> {in s1 & &, transitive leT} -> {in s1 &, antisymmetric leT} -> reflect (sort leT s1 = sort leT s2) (perm_eq s1 s2).
proof: Proof. move=> /in2_sig leT_total /in3_sig leT_tr /in2_sig/(_ _ _ _)/val_inj leT_asym. apply: (iffP idP) => s1s2; last by rewrite -(perm_sort leT) s1s2 perm_sort. move: (s1s2); have /all_sigP[s1' ->] := allss s1. have /all_sigP[{s1s2}s2 ->] : all [in s1] s2 by rewrite -(perm_all _ s1s2). by rewrite !sort_map => /(perm_map_inj val_inj) /(perm_sortP leT_total)->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)