proposition: Lemma split_findlast p s (i := findlast p s) : has p s -> split_findlast_spec p s (take i s) (drop i.+1 s).
proof: Proof. by case: s => // x ? in i * =>?; case: split_findlast_nth=>//; constructor. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)