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