proposition: Lemma slice_kk s k l r : &:s (Interval (BSide l k) (BSide r k)) = if l && ~~ r then oapp (cons^~ [::]) [::] (onth s k) else [::].
proof: Proof. rewrite /slice /=; case: (onth_sizeP s k)=>[|v] H; rewrite H /=. - move/size_onthPn: H=>H; rewrite if_same. apply: drop_oversize; rewrite size_take ltnNge. have ->/= : (size s <= k + ~~ r)%N by apply/leq_trans/leq_addr. by apply/leq_trans/leq_addr. move: (onth_size H)=>Hk; case: l; case: r=>/=; rewrite ?addn0 ?addn1. - by apply: drop_oversize; rewrite size_take Hk. - rewrite -addn1 addnC -take_drop. rewrite (take_nth v); last by rewrite size_drop subn_gt0. by rewrite take0 /= nth_drop addn0 nth_onth H. - by apply: drop_oversize; rewrite size_take Hk. apply: drop_oversize; rewrite size_take; case: ifP=>// /negbT. by rewrite -leqNgt. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)