equal
deleted
inserted
replaced
171 by (simp only: mod_div_equality') |
171 by (simp only: mod_div_equality') |
172 finally show ?thesis . |
172 finally show ?thesis . |
173 qed |
173 qed |
174 |
174 |
175 lemma dvd_imp_mod_0: "a dvd b \<Longrightarrow> b mod a = 0" |
175 lemma dvd_imp_mod_0: "a dvd b \<Longrightarrow> b mod a = 0" |
176 by (unfold dvd_def, auto) |
176 by (rule dvd_eq_mod_eq_0[THEN iffD1]) |
177 |
177 |
178 lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b" |
178 lemma dvd_div_mult_self: "a dvd b \<Longrightarrow> (b div a) * a = b" |
179 by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0) |
179 by (subst (2) mod_div_equality [of b a, symmetric]) (simp add:dvd_imp_mod_0) |
180 |
180 |
181 lemma div_dvd_div[simp]: |
181 lemma div_dvd_div[simp]: |