proposition: Lemma split_find p s (i := find p s) : has p s -> split_find_spec p s (take i s) (drop i.+1 s).
proof: Proof. by case: s => // x ? in i * => ?; case: split_find_nth => //; constructor. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)