proposition: Lemma slice_xL b x s : BRight x <= b -> &:s (Interval (BLeft x) b) = oapp (cons^~ (&:s (Interval (BRight x) b))) [::] (onth s x).
proof: Proof. move=>Hxb; rewrite (slice_split _ false (x:=x)) /=; last first. - rewrite in_itv /= lexx /=. by case: b Hxb=>/=[bx bv|bx]; case: bx. rewrite slice_kk /=; case: (onth_sizeP s x)=>[|v] H; rewrite H //=. rewrite itv_overL //= addn1; apply: ltW. by apply/size_onthPn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)