proposition: Lemma subseq_sorted_in s1 s2 : {in s2 & &, transitive leT} -> subseq s1 s2 -> sorted s2 -> sorted s1.
proof: Proof. by move=> tr /subseqP [m _ ->]; apply/(sorted_mask_in tr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)