src/HOL/Nat.thy
changeset 60353 838025c6e278
parent 60175 831ddb69db9b
child 60427 b4b672f09270
     1.1 --- a/src/HOL/Nat.thy	Mon Jun 01 18:59:21 2015 +0200
     1.2 +++ b/src/HOL/Nat.thy	Mon Jun 01 18:59:22 2015 +0200
     1.3 @@ -1484,6 +1484,14 @@
     1.4  lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
     1.5    by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
     1.6  
     1.7 +lemma of_nat_neq_0 [simp]:
     1.8 +  "of_nat (Suc n) \<noteq> 0"
     1.9 +  unfolding of_nat_eq_0_iff by simp
    1.10 +
    1.11 +lemma of_nat_0_neq [simp]:
    1.12 +  "0 \<noteq> of_nat (Suc n)"
    1.13 +  unfolding of_nat_0_eq_iff by simp  
    1.14 +  
    1.15  end
    1.16  
    1.17  context linordered_semidom