equal
deleted
inserted
replaced
1272 begin |
1272 begin |
1273 |
1273 |
1274 text{*Special cases where either operand is zero*} |
1274 text{*Special cases where either operand is zero*} |
1275 |
1275 |
1276 lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n" |
1276 lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n" |
1277 by (rule of_nat_eq_iff [of 0, simplified]) |
1277 by (rule of_nat_eq_iff [of 0 n, unfolded of_nat_0]) |
1278 |
1278 |
1279 lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0" |
1279 lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0" |
1280 by (rule of_nat_eq_iff [of _ 0, simplified]) |
1280 by (rule of_nat_eq_iff [of m 0, unfolded of_nat_0]) |
1281 |
1281 |
1282 lemma inj_of_nat: "inj of_nat" |
1282 lemma inj_of_nat: "inj of_nat" |
1283 by (simp add: inj_on_def) |
1283 by (simp add: inj_on_def) |
1284 |
1284 |
1285 end |
1285 end |