proposition: Lemma slice_count p s i : count p (&:s i) = count (fun j => j \in i) (findall p s).
proof: Proof. elim: s i=>/= [|x s IH] i; first by rewrite slice0. rewrite findall_cons slice_cons. case/boolP: (p x)=>/= Hpx; case/boolP: (0 \in i)=>I0 /=. - rewrite Hpx !add1n; congr S. rewrite IH count_map; apply: eq_count=>z /=. by rewrite mem_shl add1n. - rewrite IH /= count_map; apply: eq_count=>z /=. by rewrite mem_shl add1n. - rewrite (negbTE Hpx) /= IH /= count_map; apply: eq_count=>z /=. by rewrite mem_shl add1n. rewrite IH /= count_map; apply: eq_count=>z /=. by rewrite mem_shl add1n. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)