proposition: Lemma find_leq_last p s : find p s <= findlast p s.
proof: Proof. rewrite findlastE. case/boolP: (has p s)=>[|_]; last by apply: find_size. elim: s=>//= h s IH. rewrite rev_cons -cats1 find_cat has_rev size_rev /=. case/orP; first by move=>->. move=>/[dup] H ->; case: ifP=>_ //. rewrite subSn /=; last first. - by rewrite -size_rev; apply: find_size. apply: (leq_ltn_trans (IH H)); rewrite ltn_predL subn_gt0. by rewrite -size_rev -has_find has_rev. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)