proposition: Lemma split_find_nth x0 p s (i := find p s) : has p s -> split_find_nth_spec p s (take i s) (drop i.+1 s) (nth x0 s i).
proof: Proof. move=> p_s; rewrite -[X in split_find_nth_spec _ X](cat_take_drop i s). rewrite (drop_nth x0 _) -?has_find// -cat_rcons. by constructor; [apply: nth_find | rewrite has_take -?leqNgt]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)