proposition: Lemma eqsl_uL_notinE s b t : t \notin s -> &=s `(Interval -oo (BSide b t)) = s.
proof: Proof. move=>N; rewrite /eq_slice /= itv_overR /=; first by exact: slice_uu. 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)