src/HOL/GCD.thy
changeset 66936 cf8d8fc23891
parent 66836 4eb431c3f974
child 67051 e7e54a0b9197
     1.1 --- a/src/HOL/GCD.thy	Sun Oct 29 19:39:03 2017 +0100
     1.2 +++ b/src/HOL/GCD.thy	Mon Oct 30 13:18:41 2017 +0000
     1.3 @@ -1600,13 +1600,10 @@
     1.4      by simp
     1.5  next
     1.6    case False
     1.7 -  then have "inj (times b)"
     1.8 -    by (rule inj_times)
     1.9    show ?thesis proof (cases "finite A")
    1.10      case False
    1.11 -    moreover from \<open>inj (times b)\<close>
    1.12 -    have "inj_on (times b) A"
    1.13 -      by (rule inj_on_subset) simp
    1.14 +    moreover have "inj_on (times b) A"
    1.15 +      using \<open>b \<noteq> 0\<close> by (rule inj_on_mult)
    1.16      ultimately have "infinite (times b ` A)"
    1.17        by (simp add: finite_image_iff)
    1.18      with False show ?thesis