proposition: Lemma findlast_cons p x s : findlast p (x::s) = if p x && ~~ has p s then 0 else (findlast p s).+1.
proof: Proof. rewrite -cat1s findlast_cat /= !add1n orbF findlast1. by case: ifP=>// /andP [->]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)