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