proposition: Lemma splitLastP s x (i := indexlast x s) : x \in s -> splitLast x s (take i s) (drop i.+1 s).
proof: Proof. case: s => // y s in i * => H. case: split_findlast_nth=>//; first by rewrite has_pred1. move=>_ s1 s2 /= /eqP->; rewrite has_pred1 => H2. by constructor. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)