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