added lemma

--- a/src/HOL/List.thy	Mon Mar 15 11:50:58 2021 +0100
+++ b/src/HOL/List.thy	Mon Mar 15 22:58:20 2021 +0100
@@ -4371,6 +4371,10 @@
 lemma remove1_idem: "x \<notin> set xs \<Longrightarrow> remove1 x xs = xs"
 by (induct xs) simp_all
 
+lemma remove1_split:
+  "a \<in> set xs \<Longrightarrow> \<exists>ls rs. xs = ls @ a # rs \<and> remove1 a xs = ls @ rs"
+by (metis remove1.simps(2) remove1_append split_list_first)
+
 
 subsubsection \<open>\<^const>\<open>removeAll\<close>\<close>