equal
deleted
inserted
replaced
153 apply (rule_tac [6] zless_zprime_imp_zrelprime) |
153 apply (rule_tac [6] zless_zprime_imp_zrelprime) |
154 apply (rule_tac [8] inv_less) |
154 apply (rule_tac [8] inv_less) |
155 apply (rule_tac [7] inv_g_1 [THEN aux2]) |
155 apply (rule_tac [7] inv_g_1 [THEN aux2]) |
156 apply (unfold zprime_def) |
156 apply (unfold zprime_def) |
157 apply (auto intro: d22set_g_1 d22set_le |
157 apply (auto intro: d22set_g_1 d22set_le |
158 aux1 aux2 aux3 aux4) |
158 aux1 aux2 aux3 aux4) |
159 done |
159 done |
160 |
160 |
161 lemma inv_d22set_d22set: |
161 lemma inv_d22set_d22set: |
162 "zprime p ==> inv p ` d22set (p - 2) = d22set (p - 2)" |
162 "zprime p ==> inv p ` d22set (p - 2) = d22set (p - 2)" |
163 apply (rule endo_inj_surj) |
163 apply (rule endo_inj_surj) |