src/HOL/Library/Type_Length.thy

--- a/src/HOL/Library/Type_Length.thy	Mon Dec 02 18:29:22 2019 +0100
+++ b/src/HOL/Library/Type_Length.thy	Mon Dec 02 17:15:16 2019 +0000
@@ -103,4 +103,8 @@
 
 end
 
+lemma length_not_greater_eq_2_iff [simp]:
+  \<open>\<not> 2 \<le> LENGTH('a::len) \<longleftrightarrow> LENGTH('a) = 1\<close>
+  by (auto simp add: not_le dest: less_2_cases)
+
 end