proposition: Lemma eqsl_xuL t s : &=s `[t, +oo[ = if t \in s then t :: &=s `]t, +oo[ else &=s `]t, +oo[.
proof: Proof. rewrite /eq_slice /= (@slice_split _ _ _ false (index t s)) //=; last first. - by rewrite in_itv /= andbT. by rewrite slice_kk /= onth_index; case: ifP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)