proposition: Lemma findlast_cat p s1 s2 : findlast p (s1 ++ s2) = if has p s1 && ~~ has p s2 then findlast p s1 else size s1 + findlast p s2.
proof: Proof. rewrite !findlastE has_cat rev_cat find_cat has_rev size_cat size_rev. case/boolP: (has p s2)=>H2; last first. - rewrite orbF; case/boolP: (has p s1)=>//= H1. by rewrite addnC subnDl. have H2' : find p (rev s2) < size s2. - by rewrite -size_rev -has_find has_rev. rewrite /= orbT andbF -addnBA; last by apply: ltnW. rewrite -!subn1 -subnDA -addnBA; last by rewrite subn_gt0. by rewrite subnDA. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)