equal
deleted
inserted
replaced
1698 by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0]) |
1698 by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0]) |
1699 |
1699 |
1700 lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0" |
1700 lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0" |
1701 by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0]) |
1701 by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0]) |
1702 |
1702 |
|
1703 lemma of_nat_1_eq_iff [simp]: "1 = of_nat n \<longleftrightarrow> n=1" |
|
1704 using of_nat_eq_iff by fastforce |
|
1705 |
|
1706 lemma of_nat_eq_1_iff [simp]: "of_nat n = 1 \<longleftrightarrow> n=1" |
|
1707 using of_nat_eq_iff by fastforce |
|
1708 |
1703 lemma of_nat_neq_0 [simp]: "of_nat (Suc n) \<noteq> 0" |
1709 lemma of_nat_neq_0 [simp]: "of_nat (Suc n) \<noteq> 0" |
1704 unfolding of_nat_eq_0_iff by simp |
1710 unfolding of_nat_eq_0_iff by simp |
1705 |
1711 |
1706 lemma of_nat_0_neq [simp]: "0 \<noteq> of_nat (Suc n)" |
1712 lemma of_nat_0_neq [simp]: "0 \<noteq> of_nat (Suc n)" |
1707 unfolding of_nat_0_eq_iff by simp |
1713 unfolding of_nat_0_eq_iff by simp |