src/HOL/GCD.thy
changeset 58787 af9eb5e566dd
parent 58776 95e58e04e534
child 58834 773b378d9313
     1.1 --- a/src/HOL/GCD.thy	Sat Oct 25 19:20:28 2014 +0200
     1.2 +++ b/src/HOL/GCD.thy	Sun Oct 26 19:11:16 2014 +0100
     1.3 @@ -870,7 +870,8 @@
     1.4        by (simp add: ab'(1,2)[symmetric])
     1.5      hence "?g^n*a'^n dvd ?g^n *b'^n"
     1.6        by (simp only: power_mult_distrib mult.commute)
     1.7 -    with zn z n have th0:"a'^n dvd b'^n" by auto
     1.8 +    then have th0: "a'^n dvd b'^n"
     1.9 +      using zn by auto
    1.10      have "a' dvd a'^n" by (simp add: m)
    1.11      with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
    1.12      hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)