proposition: Lemma nth_findlast x0 p s : has p s -> p (nth x0 s (findlast p s)).
proof: Proof. rewrite findlastE=>/[dup] E ->; rewrite -has_rev in E. rewrite -subnS -nth_rev; last by rewrite -size_rev -has_find. by apply: nth_find. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)