src/HOL/Ring_and_Field.thy
changeset 33676 802f5e233e48
parent 33364 2bd12592c5e8
child 34146 14595e0c27e8
     1.1 --- a/src/HOL/Ring_and_Field.thy	Fri Nov 13 19:49:13 2009 +0100
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Nov 13 22:01:01 2009 +0100
     1.3 @@ -1301,6 +1301,10 @@
     1.4  lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
     1.5    by (simp add: abs_if)
     1.6  
     1.7 +lemma dvd_if_abs_eq:
     1.8 +  "abs l = abs (k) \<Longrightarrow> l dvd k"
     1.9 +by(subst abs_dvd_iff[symmetric]) simp
    1.10 +
    1.11  end
    1.12  
    1.13  class ordered_field = field + ordered_idom