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