proposition: Lemma subseq_sort_in t s : {in s &, total leT} -> {in s & &, transitive leT} -> subseq t s -> subseq (sort leT t) (sort leT s).
proof: Proof. move=> leT_total leT_tr /subseqP [m _ ->]. have [m' <-] := mask_sort_in leT_total leT_tr m (allss _). exact: mask_subseq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)