equal
deleted
inserted
replaced
480 lemma dvd_0_left: "0 dvd m ==> m = (0::nat)" |
480 lemma dvd_0_left: "0 dvd m ==> m = (0::nat)" |
481 by (force simp add: dvd_def) |
481 by (force simp add: dvd_def) |
482 |
482 |
483 lemma dvd_0_left_iff [iff]: "(0 dvd (m::nat)) = (m = 0)" |
483 lemma dvd_0_left_iff [iff]: "(0 dvd (m::nat)) = (m = 0)" |
484 by (blast intro: dvd_0_left) |
484 by (blast intro: dvd_0_left) |
|
485 |
|
486 declare dvd_0_left_iff [noatp] |
485 |
487 |
486 lemma dvd_1_left [iff]: "Suc 0 dvd k" |
488 lemma dvd_1_left [iff]: "Suc 0 dvd k" |
487 unfolding dvd_def by simp |
489 unfolding dvd_def by simp |
488 |
490 |
489 lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)" |
491 lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)" |