proposition: Lemma hasNfindlast p s : ~~ has p s -> findlast p s = size s.
proof: Proof. by rewrite has_findlast; case: ltngtP (findlast_size p s). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)