proposition: Lemma eqsl_xxL t1 t2 s : &=s `[t1, t2] = if (t1 <=[s] t2) && (t1 \in s) then t1 :: &=s `]t1, t2] else [::].
proof: Proof. rewrite /eq_slice /seq_le /=. case: leqP=>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 N1. by rewrite (memNindex N1) itv_overL //= addn1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)