proposition: Lemma sle_splitR x y ks1 ks2 : y \notin ks1 -> x <=[ks1++x::ks2] y.
proof: Proof. move=>Y; rewrite sle_eqVlt; last first. - by apply/orP; left; rewrite mem_cat inE eq_refl orbT. by case: eqP=>[|/eqP N] //=; rewrite (slt_splitR _ _ Y) // eq_sym. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)