proposition: Lemma slice_oSL x a s : &:s (Interval (BLeft x.+1) a) = &:s (Interval (BRight x) a).
proof: Proof. case/boolP: (x.+1 \in Interval (BRight x) a)=>[H|]. - rewrite [RHS](slice_split _ true (x:=x.+1)) //=. suff ->: &:s `]x, x.+1[ = [::] by rewrite cat0s. by rewrite /slice /= addn0 addn1 drop_take_id. rewrite in_itv /= negb_and ltEnat /= ltnS leqnn /=. case: a=>[[] a|[]] //=. - by rewrite -leNgt leEnat => H; rewrite !itv_swapped //= !addn0 ?addn1 leEnat. - by rewrite -ltNge ltEnat /= => H; rewrite !itv_swapped //= !addn1 ?addn0 leEnat ltnS. by move=>_; rewrite !itv_minfR. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)