proposition: Lemma eqsl_xoL t1 t2 s : &=s `[t1, t2[ = if t1 <[s] t2 then t1 :: &=s `]t1, t2[ else [::].
proof: Proof. rewrite /eq_slice /seq_lt /=. case: ltnP=>I; last by rewrite itv_swapped_bnd. rewrite (@slice_split _ _ _ false (index t1 s)) /=; last first. - by rewrite in_itv /= lexx. rewrite slice_kk /= onth_index; case: ifP=>//= /negbT/memNindex E. by move: I; rewrite E ltnNge index_size. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)