added lemma

--- a/src/HOL/List.thy	Sun Dec 26 11:01:27 2021 +0000
+++ b/src/HOL/List.thy	Wed Dec 29 08:07:51 2021 +0100
@@ -1244,6 +1244,9 @@
 lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"
 by(rule rev_cases[of xs]) auto
 
+lemma length_Suc_conv_rev: "(length xs = Suc n) = (\<exists>y ys. xs = ys @ [y] \<and> length ys = n)"
+by (induct xs rule: rev_induct) auto
+
 
 subsubsection \<open>\<^const>\<open>set\<close>\<close>