proposition: Corollary eqsl_notinR x b t s : t \notin s -> &=s (Interval x (BSide b t)) = &=s (Interval x +oo).
proof: Proof. move=>T; apply: eqsl_overR=>/=. by rewrite (memNindex T); apply: leq_addr. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)