proposition: Lemma eqsl_minfR s (i : itv_bound A) : &=s (Interval i -oo) = [::].
proof: Proof. by rewrite /eq_slice /=; apply: itv_minfR. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)