proposition: Lemma in_split (x : A) (s : seq A) : x \In s -> exists s1, exists s2, s = s1 ++ x :: s2.
proof: Proof. elim:s=>[|y s IH] //=; rewrite InE. case=>[<-|]; first by exists [::]; exists s. by case/IH=>s1 [s2] ->; exists (y :: s1); exists s2. Qed.
imports: mathcomp(ssreflect ssrfun seq) LemmaOverloading(rels)