proposition: Lemma findlast1 p x : findlast p [::x] = ~~ p x.
proof: Proof. by rewrite findlastE /= orbF; case: ifP=>// ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)