proposition: Lemma itv_overL s (i j : itv_bound nat) : size s <= bnd i (size s) -> &:s (Interval i j) = [::].
proof: Proof. move=>Hi /=; rewrite /slice /=; apply: drop_oversize. rewrite size_take; case: ifP=>// H. by apply/ltnW/(leq_trans H). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)