--- a/src/HOL/List.thy Sat Nov 17 16:29:09 2018 +0100
+++ b/src/HOL/List.thy Sun Nov 18 09:51:41 2018 +0100
@@ -839,6 +839,10 @@
"(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
by (induct xs; simp; blast)
+lemma Suc_le_length_iff:
+ "(Suc n \<le> length xs) = (\<exists>x ys. xs = x # ys \<and> n \<le> length ys)"
+by (metis Suc_le_D[of n] Suc_le_mono[of n] Suc_length_conv[of _ xs])
+
lemma impossible_Cons: "length xs \<le> length ys ==> xs = x # ys = False"
by (induct xs) auto