proposition: Lemma findlast_rcons p x s : findlast p (rcons s x) = if p x then size s else if has p s then findlast p s else (size s).+1.
proof: Proof. rewrite -cats1 findlast_cat /= orbF findlast1. case: (p x)=>/=; first by rewrite andbF addn0. by rewrite andbT addn1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)