proposition: Corollary findlastE p s : findlast p s = if has p s then (size s - seq.find p (rev s)).-1 else size s.
proof: Proof. rewrite /findlast findlast_auxE /= !add0n -has_rev; case/boolP: (has p (rev s)). - by rewrite has_find size_rev; case: ltngtP. by move/hasNfind=>->; rewrite size_rev eqxx. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)