proposition: Lemma has_findlast p s : has p s = (findlast p s < size s).
proof: Proof. symmetry; rewrite findlastE; case: ifP=>H /=; last by rewrite ltnn. by rewrite -subnS /= ltn_subrL /=; case: s H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)