proposition: Corollary findall_cons p x s : findall p (x::s) = if p x then 0 :: map S (findall p s) else map S (findall p s).
proof: Proof. by rewrite -cat1s findall_cat /= findallE /=; case: (p x). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)