proposition: Lemma eqsl_oxR t1 t2 s : &=s `]t1, t2] = if t1 <[s] t2 then if t2 \in s then rcons (&=s `]t1, t2[) t2 else &=s `]t1, +oo[ else [::].
proof: Proof. rewrite /eq_slice /seq_lt /=. case: ltnP=>I; last by rewrite itv_swapped_bnd. rewrite (@slice_split _ _ _ true (index t2 s)) /=; last first. - by rewrite in_itv /= lexx andbT. rewrite slice_kk /= onth_index /=; case: ifP=>/=; first by rewrite cats1. rewrite cats0 =>/negbT/memNindex->. by apply: itv_overR=>/=; rewrite addn0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)