proposition: Corollary slice_oPR a x s : &:s (Interval a (BRight x.-1)) = if 0 < x then &:s (Interval a (BLeft x)) else &:s (Interval a (BRight x)).
proof: Proof. by case: x=>//= n; rewrite slice_oSR. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)