diff -r d46de31a50c4 -r 838025c6e278 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Jun 01 18:59:21 2015 +0200
+++ b/src/HOL/Nat.thy	Mon Jun 01 18:59:22 2015 +0200
@@ -1484,6 +1484,14 @@
 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_neq_0 [simp]:
+  "of_nat (Suc n) \<noteq> 0"
+  unfolding of_nat_eq_0_iff by simp
+
+lemma of_nat_0_neq [simp]:
+  "0 \<noteq> of_nat (Suc n)"
+  unfolding of_nat_0_eq_iff by simp  
+  
 end
 
 context linordered_semidom