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