proposition: Lemma findlast_auxE oi0 p s : findlast_aux oi0 p s = let k := seq.find p (rev s) in (if k == size s then oi0.1 else Some (oi0.2 + (size s - k).-1), oi0.2 + size s).
proof: Proof. rewrite /findlast_aux; elim: s oi0=>/= [|x s IH] [o0 i0] /=; first by rewrite addn0. rewrite IH /= rev_cons -cats1 find_cat /= has_find. move: (find_size p (rev s)); rewrite size_rev; case: ltngtP=>// H _. - case: eqP=>[E|_]; first by rewrite E ltnNge leqnSn in H. apply: injective_projections=>/=; [congr Some | rewrite addSnnS]=>//. by rewrite !predn_sub /= -predn_sub addSnnS prednK // subn_gt0. case: ifP=>_; rewrite addSnnS; last by rewrite addn1 eqxx. by rewrite addn0 eqn_leq leqnSn /= ltnn subSnn addn0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)