equal
deleted
inserted
replaced
405 where "b = x * m + a" |
405 where "b = x * m + a" |
406 by fast |
406 by fast |
407 |
407 |
408 hence "b mod m = (x * m + a) mod m" by simp |
408 hence "b mod m = (x * m + a) mod m" by simp |
409 also |
409 also |
410 have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq) |
410 have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: mod_add_eq) |
411 also |
411 also |
412 have "\<dots> = a mod m" by simp |
412 have "\<dots> = a mod m" by simp |
413 finally |
413 finally |
414 have "b mod m = a mod m" . |
414 have "b mod m = a mod m" . |
415 thus "a mod m = b mod m" .. |
415 thus "a mod m = b mod m" .. |