proposition: Lemma eqsl1_uR (k : A) b t : &=[::k] (Interval (BSide b t) +oo) = if b && (t==k) then [::k] else [::].
proof: Proof. rewrite eqsl_uR_consE; case: eqVneq=>_; first by rewrite andbT. by rewrite eqslice0 andbF. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)