| changeset 13716 | 73de0ef7cb25 |
| parent 13601 | fd3e3d6b37b2 |
| child 13788 | fd03c4ab89d4 |
--- a/src/HOL/Integ/IntDiv.thy Wed Nov 13 15:36:36 2002 +0100 +++ b/src/HOL/Integ/IntDiv.thy Fri Nov 15 18:02:25 2002 +0100 @@ -628,6 +628,8 @@ declare zmod_eq_0_iff [THEN iffD1, dest!] +lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))" +by(simp add:dvd_def zmod_eq_0_iff) (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)