proposition: Lemma slice_rcons x s i : &:(rcons s x) i = if size s \in i then rcons (&:s i) x else &:s i.
proof: Proof. rewrite -cats1 slice_cat slice1 mem_shl addn0. by case: ifP=>_; [rewrite cats1 | rewrite cats0]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)