proposition: Lemma sle_subseq ks1 ks2 k t : subseq ks1 ks2 -> uniq ks2 -> k \in ks1 -> t \in ks1 -> k <=[ks1] t = k <=[ks2] t.
proof: Proof. by move=>S U T K; rewrite !sleNgt (slt_subseq S U K T). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)