proposition: Lemma slice_xR a x s : a <= BLeft x -> &:s (Interval a (BRight x)) = oapp (rcons (&:s (Interval a (BLeft x)))) (&:s (Interval a +oo)) (onth s x).
proof: Proof. move=>Hax; rewrite (slice_split _ true (x:=x)) /=; last first. - rewrite in_itv /= lexx andbT. by case: a Hax=>/=[ax av|ax]; case: ax. rewrite slice_kk /=; case: (onth_sizeP s x)=>[|v] H; rewrite H /=; last by rewrite cats1. rewrite cats0 itv_overR //= addn0. by apply/size_onthPn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)