proposition: Lemma in_split xs x : x \in xs -> exists xs1 xs2, xs = xs1 ++ x :: xs2 /\ x \notin xs1.
proof: Proof. rewrite -has_pred1; case/split_find=>_ s1 s2 /eqP ->. by rewrite has_pred1=>H; exists s1, s2; rewrite -cats1 -catA. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)