proposition: Lemma irr_sorted_eq : irreflexive leT -> forall s1 s2, sorted s1 -> sorted s2 -> s1 =i s2 -> s1 = s2.
proof: Proof. move=> leT_irr s1 s2 s1_sort s2_sort eq_s12. have: antisymmetric leT. by move=> m n /andP[? ltnm]; case/idP: (leT_irr m); apply: leT_tr ltnm. by move/sorted_eq; apply=> //; apply: uniq_perm => //; apply: sorted_uniq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)