equal
deleted
inserted
replaced
55 apply auto |
55 apply auto |
56 apply (subgoal_tac "\<not> p dvd 1") |
56 apply (subgoal_tac "\<not> p dvd 1") |
57 apply (rule_tac [2] zdvd_not_zless) |
57 apply (rule_tac [2] zdvd_not_zless) |
58 apply (subgoal_tac "p dvd 1") |
58 apply (subgoal_tac "p dvd 1") |
59 prefer 2 |
59 prefer 2 |
60 apply (subst zdvd_zminus_iff [symmetric]) |
60 apply (subst dvd_minus_iff [symmetric]) |
61 apply auto |
61 apply auto |
62 done |
62 done |
63 |
63 |
64 lemma inv_not_1: |
64 lemma inv_not_1: |
65 "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 1" |
65 "zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 1" |
77 -- {* same as @{text WilsonRuss} *} |
77 -- {* same as @{text WilsonRuss} *} |
78 apply (unfold zcong_def) |
78 apply (unfold zcong_def) |
79 apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2) |
79 apply (simp add: OrderedGroup.diff_diff_eq diff_diff_eq2 zdiff_zmult_distrib2) |
80 apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) |
80 apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) |
81 apply (simp add: mult_commute) |
81 apply (simp add: mult_commute) |
82 apply (subst zdvd_zminus_iff) |
82 apply (subst dvd_minus_iff) |
83 apply (subst zdvd_reduce) |
83 apply (subst zdvd_reduce) |
84 apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans) |
84 apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans) |
85 apply (subst zdvd_reduce) |
85 apply (subst zdvd_reduce) |
86 apply auto |
86 apply auto |
87 done |
87 done |