proposition: Lemma slice_split_bnd s (i : interval nat) (x : itv_bound nat) : i.1 <= x <= i.2 -> &:s i = &:s (Interval i.1 x) ++ &:s (Interval x i.2).
proof: Proof. case: i=>i1 i2 /=. case: x=>[b x|[]]; rewrite ?bnd_simp /=; first last. - by move/eqP=>->; rewrite itv_pinfL cats0. - by rewrite andbT =>/eqP->; rewrite itv_minfR. case/boolP: (size s <= bnd (BSide b x) (size s)). - move=>H Hx; rewrite (itv_overL _ H) cats0 (itv_overR _ H). apply: itv_overR; rewrite /= in H. case/andP: Hx=>_. case: i2=>[[] i2|[]] //= Hx; apply: (leq_trans H); case: {H}b Hx; rewrite bnd_simp ?addn0 ?addn1 //. by move=>Hx; apply/ltnW. rewrite -ltNge ltEnat /= =>/ltnW/minn_idPl Hx. case: i1=>[l i|[]]; case: i2=>[r j|[]] //=; rewrite ?bnd_simp ?andbF ?andbT // ?lteBSide /slice /= ?drop0 ?take_size. - case/andP=>Hi Hj. have Hxj : (x + ~~ b <= j + ~~r)%N. - case: r Hj=>/=; rewrite ?leEnat ?ltEnat; case: {Hx Hi}b=>/=; rewrite ?addn0 ?addn1 // => Hj; by apply: ltnW. have Hxi : (i + ~~ l <= x + ~~ b)%N. - case: l Hi=>/=; rewrite ?implybT ?implybF /= ?addn0 ?addn1 /= => Hi. - by apply/(leq_trans Hi)/leq_addr. by case: {Hx Hj Hxj}b Hi=>/=; rewrite ?leEnat ?ltEnat /= ?addn0 ?addn1. rewrite -{1}(subnKC Hxj) takeD drop_cat size_take_min Hx take_drop subnK //. rewrite ltn_neqAle Hxi andbT; case: eqP=>//= ->. by rewrite subnn drop0 drop_take_id. - move=>Hi; rewrite -{1}(cat_take_drop (x + ~~ b) s) drop_cat size_take_min Hx. have Hxi : (i + ~~ l <= x + ~~ b)%N. - case: l Hi=>/=; rewrite ?implybT ?implybF /= ?addn0 ?addn1 /= => Hi. - by apply/(leq_trans Hi)/leq_addr. by case: {Hx}b Hi=>/=; rewrite ?leEnat ?ltEnat /= ?addn0 ?addn1. rewrite ltn_neqAle Hxi andbT; case: eqP=>//= ->. by rewrite subnn drop0 drop_take_id. - move=>Hj. have Hbj : (x + ~~ b <= j + ~~ r)%N. - case: r Hj=>/=; rewrite ?leEnat ?ltEnat; case: {Hx}b=>/=; rewrite ?addn0 ?addn1 // => Hx; by apply: ltnW. by rewrite -{1}(subnKC Hbj) takeD take_drop subnK. by move=>_; rewrite cat_take_drop. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)