proposition: Lemma sorted_subset_subseq (s1 s2 : seq A) ltT : irreflexive ltT -> transitive ltT -> sorted ltT s1 -> sorted ltT s2 -> {subset s1 <= s2} -> subseq s1 s2.
proof: Proof. move=>R T S1 S2 H. suff -> : s1 = filter (fun x => x \in s1) s2 by apply: filter_subseq. apply: irr_sorted_eq S1 _ _=>//; first by rewrite sorted_filter. by move=>k; rewrite mem_filter; case S : (_ \in _)=>//; rewrite (H _ S). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)