proposition: Lemma sorted_subseq_sort_in t s : {in s &, total leT} -> {in s & &, transitive leT} -> subseq t s -> sorted leT t -> subseq t (sort leT s).
proof: Proof. move=> ? leT_tr ? /(sorted_sort_in leT_tr) <-; last exact/allP/mem_subseq. exact: subseq_sort_in. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)