proposition: Lemma sorted_subseqP s1 s2 : transitive leT -> irreflexive leT -> sorted leT s1 -> sorted leT s2 -> reflect {subset s1 <= s2} (subseq s1 s2).
proof: Proof. move=> leT_trans leT_irr s1_sort s2_sort. apply (iffP idP) => [|sub_s12]; first exact: mem_subseq. apply/subseqP; exists [seq i \in s1 | i <- s2]; first by rewrite size_map. apply: (irr_sorted_eq leT_trans leT_irr s1_sort). exact: (sorted_mask leT_trans). move=> i; rewrite -filter_mask mem_filter. by case: (boolP (i \in s1)) => // /sub_s12 ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted