# HG changeset patch
# User nipkow
# Date 1640761671 -3600
# Node ID 8a378e99d9a88d248b83f72e29309b3c899b475d
# Parent  9469d922368930243378b4337a59138110def174
added lemma

diff -r 9469d9223689 -r 8a378e99d9a8 src/HOL/List.thy
--- 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>