proposition: Lemma itv_underL s (i j : itv_bound nat) : bnd i (size s) = 0%N -> &:s (Interval i j) = &:s (Interval -oo j).
proof: Proof. by move=>Hi; rewrite /slice /= Hi drop0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)