equal
deleted
inserted
replaced
72 done |
72 done |
73 |
73 |
74 lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)" |
74 lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)" |
75 -- {* same as @{text WilsonRuss} *} |
75 -- {* same as @{text WilsonRuss} *} |
76 apply (unfold zcong_def) |
76 apply (unfold zcong_def) |
77 apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2) |
77 apply (simp add: diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2) |
78 apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) |
78 apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) |
79 apply (simp add: mult_commute) |
79 apply (simp add: algebra_simps) |
80 apply (subst dvd_minus_iff) |
80 apply (subst dvd_minus_iff) |
81 apply (subst zdvd_reduce) |
81 apply (subst zdvd_reduce) |
82 apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans) |
82 apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans) |
83 apply (subst zdvd_reduce) |
83 apply (subst zdvd_reduce) |
84 apply auto |
84 apply auto |