proposition: Lemma itv_overR s (i j : itv_bound nat) : size s <= bnd j (size s) -> &:s (Interval i j) = &:s (Interval i +oo).
proof: Proof. by move=>Hj; rewrite /slice /= take_size take_oversize. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)