equal
deleted
inserted
replaced
141 { fix u |
141 { fix u |
142 from w_def have "u mod w < w" by simp |
142 from w_def have "u mod w < w" by simp |
143 then have "u + (w - u mod w) = w + (u - u mod w)" |
143 then have "u + (w - u mod w) = w + (u - u mod w)" |
144 by simp |
144 by simp |
145 then have "u + (w - u mod w) = w + u div w * w" |
145 then have "u + (w - u mod w) = w + u div w * w" |
146 by (simp add: div_mod_equality' [symmetric]) |
146 by (simp add: minus_mod_eq_div_mult) |
147 } |
147 } |
148 then have "w dvd v + w + r + (w - v mod w) \<longleftrightarrow> w dvd m + w + r + (w - m mod w)" |
148 then have "w dvd v + w + r + (w - v mod w) \<longleftrightarrow> w dvd m + w + r + (w - m mod w)" |
149 by (simp add: add.assoc add.left_commute [of m] add.left_commute [of v] |
149 by (simp add: add.assoc add.left_commute [of m] add.left_commute [of v] |
150 dvd_add_left_iff dvd_add_right_iff) |
150 dvd_add_left_iff dvd_add_right_iff) |
151 moreover from q have "Suc q = m + w + r" by (simp add: w_def) |
151 moreover from q have "Suc q = m + w + r" by (simp add: w_def) |