src/HOL/NumberTheory/Chinese.thy
changeset 20432 07ec57376051
parent 20272 0ca998e83447
child 21404 eb85850d3eb7
     1.1 --- a/src/HOL/NumberTheory/Chinese.thy	Tue Aug 29 21:43:34 2006 +0200
     1.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Wed Aug 30 03:19:08 2006 +0200
     1.3 @@ -175,6 +175,11 @@
     1.4       apply (rule_tac [!] funprod_zgcd)
     1.5       apply safe
     1.6       apply simp_all
     1.7 +   apply (subgoal_tac "i<n")
     1.8 +    prefer 2
     1.9 +    apply arith
    1.10 +   apply (case_tac [2] i)
    1.11 +    apply simp_all
    1.12    done
    1.13  
    1.14  lemma x_sol_lin_aux: