src/HOL/Int.thy
changeset 58649 a62065b5e1e2
parent 58512 dc4d76dfa8f0
child 58650 1ddba8bcbb58
     1.1 --- a/src/HOL/Int.thy	Sun Oct 12 16:31:43 2014 +0200
     1.2 +++ b/src/HOL/Int.thy	Sun Oct 12 17:05:34 2014 +0200
     1.3 @@ -1242,19 +1242,10 @@
     1.4  qed
     1.5  
     1.6  lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
     1.7 -  apply (subgoal_tac "m = n + (m - n)")
     1.8 -   apply (erule ssubst)
     1.9 -   apply (blast intro: dvd_add, simp)
    1.10 -  done
    1.11 +  using dvd_add_right_iff [of k "- n" m] by simp 
    1.12  
    1.13  lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
    1.14 -apply (rule iffI)
    1.15 - apply (erule_tac [2] dvd_add)
    1.16 - apply (subgoal_tac "n = (n + k * m) - k * m")
    1.17 -  apply (erule ssubst)
    1.18 -  apply (erule dvd_diff)
    1.19 -  apply(simp_all)
    1.20 -done
    1.21 +  using dvd_add_times_triv_right_iff [of k n m] by (simp add: ac_simps)
    1.22  
    1.23  lemma dvd_imp_le_int:
    1.24    fixes d i :: int