proposition: Corollary findall_rcons p x s : findall p (rcons s x) = if p x then rcons (findall p s) (size s) else findall p s.
proof: Proof. rewrite -cats1 findall_cat /= !findallE /=; case: (p x)=>/=. - by rewrite addn0 cats1. by rewrite cats0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)