equal
deleted
inserted
replaced
1197 with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"] |
1197 with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"] |
1198 have dble: "d*b \<le> x*b*(b - 1)" using bp by simp |
1198 have dble: "d*b \<le> x*b*(b - 1)" using bp by simp |
1199 from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)" |
1199 from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)" |
1200 by simp |
1200 by simp |
1201 hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x" |
1201 hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x" |
1202 by (simp only: mult_assoc right_distrib) |
1202 by (simp only: mult_assoc distrib_left) |
1203 hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)" |
1203 hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)" |
1204 by algebra |
1204 by algebra |
1205 hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp |
1205 hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp |
1206 hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)" |
1206 hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)" |
1207 by (simp only: diff_add_assoc[OF dble, of d, symmetric]) |
1207 by (simp only: diff_add_assoc[OF dble, of d, symmetric]) |