proposition: Lemma mem2_sort s x y : leT x y -> mem2 s x y -> mem2 (sort leT s) x y.
proof: Proof. move=> lexy /[!mem2E] /subseq_sort. by case: eqP => // _; rewrite {1}/sort /= lexy /=. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)