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