proposition: Corollary slice_memE1 x s i : (count_mem x s <= 1)%N -> x \in &:s i = (x \in s) && (bnd i.1 (size s) <= index x s < bnd i.2 (size s)).
proof: Proof. move=>H; rewrite slice_memE indexall_count1 //; case: ifP=>//= Hx; rewrite orbF. by case: i=>/= [[[] i|[]][[] j|[]]]; rewrite in_itv /= ?ltEnat ?leEnat /= ?ltn0 ?addn0 ?addn1 ?andbT ?andbF // ?(leqNgt (size _)) index_mem Hx //= andbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)