equal
deleted
inserted
replaced
173 apply safe |
173 apply safe |
174 apply (tactic {* stac (thm "zgcd_zmult_cancel") 3 *}) |
174 apply (tactic {* stac (thm "zgcd_zmult_cancel") 3 *}) |
175 apply (rule_tac [!] funprod_zgcd) |
175 apply (rule_tac [!] funprod_zgcd) |
176 apply safe |
176 apply safe |
177 apply simp_all |
177 apply simp_all |
|
178 apply (subgoal_tac "i<n") |
|
179 prefer 2 |
|
180 apply arith |
|
181 apply (case_tac [2] i) |
|
182 apply simp_all |
178 done |
183 done |
179 |
184 |
180 lemma x_sol_lin_aux: |
185 lemma x_sol_lin_aux: |
181 "0 < n ==> i \<le> n ==> j \<le> n ==> j \<noteq> i ==> mf j dvd mhf mf n i" |
186 "0 < n ==> i \<le> n ==> j \<le> n ==> j \<noteq> i ==> mf j dvd mhf mf n i" |
182 apply (unfold mhf_def) |
187 apply (unfold mhf_def) |