equal
deleted
inserted
replaced
129 moreover have "a div b = a div b" .. |
129 moreover have "a div b = a div b" .. |
130 moreover have "a mod b = a mod b" .. |
130 moreover have "a mod b = a mod b" .. |
131 note that ultimately show thesis by blast |
131 note that ultimately show thesis by blast |
132 qed |
132 qed |
133 |
133 |
134 lemma dvd_eq_mod_eq_0 [code unfold]: "a dvd b \<longleftrightarrow> b mod a = 0" |
134 lemma dvd_eq_mod_eq_0 [code_unfold]: "a dvd b \<longleftrightarrow> b mod a = 0" |
135 proof |
135 proof |
136 assume "b mod a = 0" |
136 assume "b mod a = 0" |
137 with mod_div_equality [of b a] have "b div a * a = b" by simp |
137 with mod_div_equality [of b a] have "b div a * a = b" by simp |
138 then have "b = a * (b div a)" unfolding mult_commute .. |
138 then have "b = a * (b div a)" unfolding mult_commute .. |
139 then have "\<exists>c. b = a * c" .. |
139 then have "\<exists>c. b = a * c" .. |