--- a/src/HOL/Nat.thy Tue Apr 25 21:31:28 2017 +0200
+++ b/src/HOL/Nat.thy Wed Apr 26 15:53:35 2017 +0100
@@ -1700,6 +1700,12 @@
lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
+lemma of_nat_1_eq_iff [simp]: "1 = of_nat n \<longleftrightarrow> n=1"
+ using of_nat_eq_iff by fastforce
+
+lemma of_nat_eq_1_iff [simp]: "of_nat n = 1 \<longleftrightarrow> n=1"
+ using of_nat_eq_iff by fastforce
+
lemma of_nat_neq_0 [simp]: "of_nat (Suc n) \<noteq> 0"
unfolding of_nat_eq_0_iff by simp