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