equal
deleted
inserted
replaced
336 lemma zcong_zless_imp_eq: |
336 lemma zcong_zless_imp_eq: |
337 "0 \<le> a ==> |
337 "0 \<le> a ==> |
338 a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b" |
338 a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b" |
339 apply (unfold zcong_def dvd_def, auto) |
339 apply (unfold zcong_def dvd_def, auto) |
340 apply (drule_tac f = "\<lambda>z. z mod m" in arg_cong) |
340 apply (drule_tac f = "\<lambda>z. z mod m" in arg_cong) |
341 apply (cut_tac z = a and w = b in zless_linear, auto) |
341 apply (cut_tac x = a and y = b in linorder_less_linear, auto) |
342 apply (subgoal_tac [2] "(a - b) mod m = a - b") |
342 apply (subgoal_tac [2] "(a - b) mod m = a - b") |
343 apply (rule_tac [3] mod_pos_pos_trivial, auto) |
343 apply (rule_tac [3] mod_pos_pos_trivial, auto) |
344 apply (subgoal_tac "(m + (a - b)) mod m = m + (a - b)") |
344 apply (subgoal_tac "(m + (a - b)) mod m = m + (a - b)") |
345 apply (rule_tac [2] mod_pos_pos_trivial, auto) |
345 apply (rule_tac [2] mod_pos_pos_trivial, auto) |
346 done |
346 done |