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