proposition: Lemma eqsl_catE s1 s2 b1 t1 b2 t2 : &= (s1 ++ s2) (Interval (BSide b1 t1) (BSide b2 t2)) = if t1 \in s1 then if t2 \in s1 then &= s1 (Interval (BSide b1 t1) (BSide b2 t2)) else &= s1 (Interval (BSide b1 t1) +oo) ++ &= s2 (Interval -oo (BSide b2 t2)) else if t2 \in s1 then [::] else &= s2 (Interval (BSide b1 t1) (BSide b2 t2)).
proof: Proof. rewrite /eq_slice slice_cat /= !index_cat. case/boolP: (t1 \in s1)=>H1; case/boolP: (t2 \in s1)=>H2. - by rewrite !index_mem H1 H2 itv_minfR cats0. - rewrite index_mem H1 ltnNge leq_addr /= itv_overR /=; last by rewrite -addnA; exact: leq_addr. by congr (_ ++ _); rewrite addnC addnK. - by rewrite ltnNge leq_addr /= index_mem H2 itv_minfR cats0 itv_overL //= -addnA; exact: leq_addr. rewrite !ltnNge !leq_addr /= itv_overL /=; last by rewrite -addnA; exact: leq_addr. by do 2!rewrite addnC addnK. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)