proposition: Lemma split_findlast_nth x0 p s (i := findlast p s) : has p s -> split_findlast_nth_spec p s (take i s) (drop i.+1 s) (nth x0 s i).
proof: Proof. move=> p_s; rewrite -[X in split_findlast_nth_spec _ X](cat_take_drop i s). rewrite (drop_nth x0 _); last by rewrite -has_findlast. rewrite -cat_rcons; constructor; first by apply: nth_findlast. by rewrite has_drop // ltnn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)