equal
deleted
inserted
replaced
441 apply (unfold cong_int_def) |
441 apply (unfold cong_int_def) |
442 apply (subgoal_tac "a * b = (-a * -b)") |
442 apply (subgoal_tac "a * b = (-a * -b)") |
443 apply (erule ssubst) |
443 apply (erule ssubst) |
444 apply (subst zmod_zmult2_eq) |
444 apply (subst zmod_zmult2_eq) |
445 apply (auto simp add: mod_add_left_eq mod_minus_right div_minus_right) |
445 apply (auto simp add: mod_add_left_eq mod_minus_right div_minus_right) |
446 apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 semiring_numeral_div_class.diff_zero)+ |
446 apply (metis mod_diff_left_eq mod_diff_right_eq mod_mult_self1_is_0 diff_zero)+ |
447 done |
447 done |
448 |
448 |
449 lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))" |
449 lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))" |
450 apply (cases "a = 0", force) |
450 apply (cases "a = 0", force) |
451 by (metis cong_altdef_nat leI less_one) |
451 by (metis cong_altdef_nat leI less_one) |