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