proposition: Lemma slice_cat s1 s2 i : &:(s1++s2) i = &:s1 i ++ &:s2 (shl_itv i (size s1)).
proof: Proof. rewrite /slice; case: i=>[[l i|[]][r j|[]]] /=; rewrite ?take0 ?drop0 ?take_size ?drop_size // ?size_cat. - rewrite take_cat; case: ltnP=>Hj. - have ->/=: (j < size s1)%N by apply/leq_ltn_trans/Hj/leq_addr. by rewrite take0 /= cats0. rewrite (take_oversize (s:=s1)) //. move: Hj; rewrite leq_eqVlt; case/orP=>[/eqP Ej|Hj]. - rewrite -Ej subnn take0 cats0 /=. case: r Ej=>/=. - by rewrite addn0=>->; rewrite ltnn subnn /= take0 /= cats0. by rewrite addn1=>->; rewrite !ltnS leqnn /= take0 /= cats0. rewrite (ltnNge j); have H1: (size s1 <= j)%N. - by case: r Hj=>/=; rewrite ?addn1 // addn0 => /ltnW. rewrite H1 drop_cat; case: ltnP=>Hi /=. - have ->/=: (i < size s1)%N by apply/leq_ltn_trans/Hi/leq_addr. by rewrite drop0 addnBAC. rewrite (drop_oversize (s:=s1)) //=. move: Hi; rewrite leq_eqVlt; case/orP=>[/eqP Ei|Hi]. - rewrite -Ei subnn drop0 /=. case: l Ei=>/=. - by rewrite addn0=><-; rewrite ltnn subnn /= drop0 addnBAC. by rewrite addn1=><-; rewrite leqnn /= drop0 addnBAC. rewrite (ltnNge i); have H2: (size s1 <= i)%N. - by case: l Hi=>/=; rewrite ?addn1 // addn0 => /ltnW. by rewrite H2 /= !addnBAC. - rewrite drop_cat; case: ltnP=>Hi /=. - have ->/=: (i < size s1)%N by apply/leq_ltn_trans/Hi/leq_addr. by rewrite drop0. rewrite (drop_oversize (s:=s1)) //=. move: Hi; rewrite leq_eqVlt; case/orP=>[/eqP Ei|Hi]. - rewrite -Ei subnn drop0 /=. case: l Ei=>/=. - by rewrite addn0=><-; rewrite ltnn subnn /= drop0. by rewrite addn1=><-; rewrite leqnn /= drop0. rewrite (ltnNge i); have H2: (size s1 <= i)%N. - by case: l Hi=>/=; rewrite ?addn1 // addn0 => /ltnW. by rewrite H2 /= addnBAC. - rewrite take_cat; case: ltnP=>Hj. - have ->/=: (j < size s1)%N by apply/leq_ltn_trans/Hj/leq_addr. by rewrite take0 /= cats0. rewrite (take_oversize (s:=s1)) //. move: Hj; rewrite leq_eqVlt; case/orP=>[/eqP Ej|Hj]. - rewrite -Ej subnn take0 cats0 /=. case: r Ej=>/=. - by rewrite addn0=>->; rewrite ltnn subnn /= take0 /= cats0. by rewrite addn1=>->; rewrite !ltnS leqnn /= take0 /= cats0. rewrite (ltnNge j); have H1: (size s1 <= j)%N. - by case: r Hj=>/=; rewrite ?addn1 // addn0 => /ltnW. by rewrite H1 /= addnBAC. by rewrite !drop_oversize //= size_take_min ?size_cat; apply: geq_minr. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)