proposition: Lemma eqsl_uL_catE s1 s2 b t : &= (s1 ++ s2) (Interval -oo (BSide b t)) = if t \in s1 then &= s1 (Interval -oo (BSide b t)) else s1 ++ &= s2 (Interval -oo (BSide b t)).
proof: Proof. rewrite /eq_slice slice_cat /= index_cat; case: ifP=>H1. - by rewrite index_mem H1 itv_minfR cats0. rewrite ltnNge leq_addr /= addnC addnK itv_overR /=; first by rewrite slice_uu. by rewrite -addnA addnCA; exact: leq_addr. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)