proposition: Lemma findlast_size p s : findlast p s <= size s.
proof: Proof. rewrite findlastE; case: ifP=>// _. by rewrite -subnS; apply: leq_subr. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)