proposition: Lemma subseq_sort : {homo sort leT : t s / subseq t s}.
proof: Proof. move=> _ s /subseqP [m _ ->]; have [m' <-] := mask_sort leT_total leT_tr s m. exact: mask_subseq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)