equal
deleted
inserted
replaced
1482 by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0]) |
1482 by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0]) |
1483 |
1483 |
1484 lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0" |
1484 lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0" |
1485 by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0]) |
1485 by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0]) |
1486 |
1486 |
|
1487 lemma of_nat_neq_0 [simp]: |
|
1488 "of_nat (Suc n) \<noteq> 0" |
|
1489 unfolding of_nat_eq_0_iff by simp |
|
1490 |
|
1491 lemma of_nat_0_neq [simp]: |
|
1492 "0 \<noteq> of_nat (Suc n)" |
|
1493 unfolding of_nat_0_eq_iff by simp |
|
1494 |
1487 end |
1495 end |
1488 |
1496 |
1489 context linordered_semidom |
1497 context linordered_semidom |
1490 begin |
1498 begin |
1491 |
1499 |