proposition: Lemma perm_sortP (T : eqType) (leT : rel T) : total leT -> transitive leT -> antisymmetric leT -> forall s1 s2, reflect (sort leT s1 = sort leT s2) (perm_eq s1 s2).
proof: Proof. move=> leT_total leT_tr leT_asym s1 s2. apply: (iffP idP) => eq12; last by rewrite -(perm_sort leT) eq12 perm_sort. apply: (sorted_eq leT_tr leT_asym); rewrite ?sort_sorted //. by rewrite perm_sort (permPl eq12) -(perm_sort leT). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)