proposition: Corollary itv_under0R s (i : itv_bound nat) : &:s (Interval i (BLeft 0%N)) = [::].
proof: Proof. by apply: itv_underR. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)