proposition: Lemma eqsl_uR_catE s1 s2 b t : &= (s1 ++ s2) (Interval (BSide b t) +oo) = if t \in s1 then &= s1 (Interval (BSide b t) +oo) ++ s2 else &= s2 (Interval (BSide b t) +oo).
proof: Proof. rewrite /eq_slice slice_cat /= index_cat; case: ifP=>H1. - by rewrite index_mem H1 slice_uu. rewrite ltnNge leq_addr /= addnC addnK itv_overL //=. 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)