proposition: Lemma mem2_sort_in s : {in s &, total leT} -> {in s & &, transitive leT} -> forall x y, leT x y -> mem2 s x y -> mem2 (sort leT s) x y.
proof: Proof. move=> leT_total leT_tr x y lexy; rewrite !mem2E. by move/subseq_sort_in; case: (_ == _); rewrite /sort /= ?lexy; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)