proposition: Lemma slice_cat_piecewise s1 s2 i : &:(s1++s2) i = if size s1 \in i then &:s1 (Interval i.1 +oo) ++ &:s2 (Interval -oo (shl_bnd i.2 (size s1))) else if bnd i.2 (size s1 + size s2) <= size s1 then &:s1 i else &:s2 (shl_itv i (size s1)).
proof: Proof. rewrite slice_cat; case: i=>i j /=; case: ifP. - rewrite in_itv; case/andP=>Hi Hj. rewrite (itv_overR _ (j:=j)); last first. - case: j Hj=>[[] j|[]] //=. - by rewrite addn0; move/ltnW. by rewrite addn1 leEnat; move/(ltnW (n:=j.+1)). rewrite (itv_underL (i:=shl_bnd i _)) //. case: i Hi=>[[] i|[]] //=; last by rewrite ltEnat /=; move=>->. rewrite leEnat leq_eqVlt; case/orP=>[/eqP->|->] //=. by rewrite ltnn /= subnn. rewrite in_itv=>/negbT; rewrite negb_and=>H. case: ifP=>Hj. - rewrite (itv_underR (s:=s2)); first by rewrite cats0. case: {H}j Hj=>[[] j|[]] //=. - rewrite addn0 leEnat leq_eqVlt; case/orP=>[/eqP->|->] //=. by rewrite ltnn /= subnn. - by rewrite addn1 leEnat =>->. by rewrite leEnat -{2}(addn0 (size s1)) leq_add2l leqn0 => /eqP. case/orP: H; last first. - case: j Hj=>[[] j|[]] //=. - by rewrite addn0 -leNgt=>->. by rewrite leEnat addn1 -ltnNge =>->. case: i=>[[] i|[]] //=; last by rewrite !itv_pinfL. - rewrite leEnat -ltnNge => Hi. rewrite (ltnNge i) (ltnW Hi) /= itv_overL //= addn0 leEnat. by apply: ltnW. rewrite ltEnat /= -leqNgt => Hi. rewrite ltnNge Hi /= itv_overL //= addn1 leEnat. by apply: ltnW. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)