proposition: Lemma slice_cons x s i : &:(x::s) i = if 0%N \in i then x::&:s (shl_itv i 1) else &:s (shl_itv i 1).
proof: Proof. by rewrite -cat1s slice_cat /= slice1; case: ifP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)