src/HOL/GCD.thy
changeset 58834 773b378d9313
parent 58787 af9eb5e566dd
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/GCD.thy	Thu Oct 30 16:36:44 2014 +0000
     1.2 +++ b/src/HOL/GCD.thy	Thu Oct 30 21:02:01 2014 +0100
     1.3 @@ -584,8 +584,8 @@
     1.4    from dvdg dvdg' obtain ka kb ka' kb' where
     1.5        kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
     1.6      unfolding dvd_def by blast
     1.7 -  then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
     1.8 -    by simp_all
     1.9 +  from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
    1.10 +    by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
    1.11    then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
    1.12      by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
    1.13        dvd_mult_div_cancel [OF dvdg(2)] dvd_def)