proposition: Lemma slt_splitL ks x y : reflect (exists ks1 ks2, [/\ ks = ks1++x::ks2, x != y, x \notin ks1 & y \notin ks1]) (x <[ks] y).
proof: Proof. case H : (x <[ks] y); constructor; last first. - apply/contraFnot: H; case=>ks1 [ks2][-> N _]. by apply: slt_splitR; rewrite eq_sym. have : x \in ks by rewrite -index_mem (leq_trans H _) // index_size. case/in_split=>ks1 [ks2][E X]; exists ks1, ks2. rewrite /seq_lt {ks}E !index_cat /= eq_refl in H *. case: eqP H=>[->|/eqP N] /=; first by rewrite ltnn. rewrite (negbTE X) addn0; case: ifP=>//= _. by rewrite ltnNge index_size. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)