proposition: Lemma sle_splitL ks x y : x \in ks -> reflect (exists ks1 ks2, [/\ ks = ks1++x::ks2, x \notin ks1 & y \notin ks1]) (x <=[ks] y).
proof: Proof. move=>X; case H : (x <=[ks] y); constructor; last first. - apply/contraFnot: H; case=>ks1 [ks2][-> _ N]. by apply: sle_splitR. case/in_split: X=>ks1 [ks2][E X]; exists ks1, ks2; split=>//. rewrite /seq_le {ks}E !index_cat /= eq_refl (negbTE X) addn0 in H. by case: ifP H=>//; rewrite -index_mem; case: ltngtP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)