src/HOL/Rings.thy
changeset 58649 a62065b5e1e2
parent 58647 fce800afeec7
child 58776 95e58e04e534
     1.1 --- a/src/HOL/Rings.thy	Sun Oct 12 16:31:43 2014 +0200
     1.2 +++ b/src/HOL/Rings.thy	Sun Oct 12 17:05:34 2014 +0200
     1.3 @@ -228,15 +228,15 @@
     1.4    "a dvd b + a \<longleftrightarrow> a dvd b"
     1.5    using dvd_add_times_triv_right_iff [of a b 1] by simp
     1.6  
     1.7 -lemma dvd_add_eq_right:
     1.8 +lemma dvd_add_right_iff:
     1.9    assumes "a dvd b"
    1.10    shows "a dvd b + c \<longleftrightarrow> a dvd c"
    1.11    using assms by (auto dest: dvd_addD)
    1.12  
    1.13 -lemma dvd_add_eq_left:
    1.14 +lemma dvd_add_left_iff:
    1.15    assumes "a dvd c"
    1.16    shows "a dvd b + c \<longleftrightarrow> a dvd b"
    1.17 -  using assms dvd_add_eq_right [of a c b] by (simp add: ac_simps)
    1.18 +  using assms dvd_add_right_iff [of a c b] by (simp add: ac_simps)
    1.19  
    1.20  end
    1.21