proposition: Lemma findall_last p s : findlast p s = last (size s) (findall p s).
proof: Proof. elim/last_ind: s=>//=s x IH; rewrite findall_rcons findlast_rcons size_rcons. case: (p x)=>/=; first by rewrite last_rcons. by rewrite IH -(negbK (has _ _)) -findall_nilp; case: (findall p s). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)