proposition: Corollary eqslice_split_full s b (x : A) : s = &=s (Interval -oo (BSide b x)) ++ &=s (Interval (BSide b x) +oo).
proof: Proof. by rewrite -[LHS](eqsl_uu s); apply: eqslice_split. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)