proposition: Lemma sorted_subseq_sort t s : subseq t s -> sorted leT t -> subseq t (sort leT s).
proof: Proof. by move=> subseq_ts /(sorted_sort leT_tr) <-; exact: subseq_sort. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)