proposition: Lemma splitP p x (i := index x p) : x \in p -> split x p (take i p) (drop i.+1 p).
proof: Proof. by rewrite -has_pred1 => /split_find[? ? ? /eqP->]; constructor. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)