proposition: Lemma findall_size p s : size (findall p s) = count p s.
proof: Proof. by elim: s=>//=x s IH; rewrite findall_cons; case: (p x)=>/=; rewrite size_map IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)