author | nipkow |
Fri, 15 Nov 2002 18:02:25 +0100 | |
changeset 13716 | 73de0ef7cb25 |
parent 13715 | 61bfaa892a41 |
child 13717 | 78f91fcdf560 |
--- 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) **)