proposition: Lemma eqsl_uR_notinE s b t : t \notin s -> &=s `(Interval (BSide b t) +oo) = [::].
proof: Proof. move=>N; rewrite /eq_slice /= itv_overL //=. by rewrite (memNindex N); exact: leq_addr. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)