proposition: Lemma slice1 (k : A) i : &:[::k] i = if 0%N \in i then [::k] else [::].
proof: Proof. rewrite /slice in_itv /=. case: i=>[[[] i|[]][[] j|[]]] //=; rewrite ?drop0 ?addn0 ?addn1 ?andbF ?andbT //=. - case: j=>[|j]/=; first by rewrite ltxx andbF. by rewrite andbT; case: i. - by case: i. - by case: i. - by apply: drop_oversize; rewrite size_take /=; case: ifP=>//; case: j. - by case: j. by case: j. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)