proposition: Lemma In_split x s : x \In s -> exists s1 s2, s = s1 ++ x :: s2.
proof: Proof. elim:s=>[|y s IH] //=; rewrite InE. case=>[<-|]; first by exists [::], s. by case/IH=>s1 [s2 ->]; exists (y :: s1), s2. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)