proposition: Lemma sorted_eq : antisymmetric leT -> forall s1 s2, sorted s1 -> sorted s2 -> perm_eq s1 s2 -> s1 = s2.
proof: Proof. by move=> leT_asym s1 s2; rewrite !sorted_pairwise //; apply: pairwise_eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)