diff -r d8fb621fea02 -r 9edb7fb69bc2 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Tue Feb 11 12:55:35 2020 +0000
+++ b/src/HOL/Num.thy	Mon Feb 17 11:07:09 2020 +0000
@@ -1107,8 +1107,11 @@
 lemma less_2_cases: "n < 2 \<Longrightarrow> n = 0 \<or> n = Suc 0"
   by (auto simp add: numeral_2_eq_2)
 
+lemma less_2_cases_iff: "n < 2 \<longleftrightarrow> n = 0 \<or> n = Suc 0"
+  by (auto simp add: numeral_2_eq_2)
+
 text \<open>Removal of Small Numerals: 0, 1 and (in additive positions) 2.\<close>
-text \<open>bh: Are these rules really a good idea?\<close>
+text \<open>bh: Are these rules really a good idea? LCP: well, it already happens for 0 and 1!\<close>
 
 lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
   by simp