proposition: Lemma eqsl1_uL (k : A) b t : &=[::k] (Interval -oo (BSide b t)) = if ~~ b || (t!=k) then [::k] else [::].
proof: Proof. rewrite eqsl_uL_consE; case: eqVneq=>_. - by rewrite orbF; case: b. by rewrite orbT eqslice0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)