src/HOL/Divides.thy
changeset 58511 97aec08d6f28
parent 58410 6d46ad54a2ab
child 58646 cd63a4b12a33
     1.1 --- a/src/HOL/Divides.thy	Thu Oct 02 11:33:04 2014 +0200
     1.2 +++ b/src/HOL/Divides.thy	Thu Oct 02 11:33:05 2014 +0200
     1.3 @@ -2425,16 +2425,6 @@
     1.4  
     1.5  subsubsection {* The Divides Relation *}
     1.6  
     1.7 -lemma dvd_neg_numeral_left [simp]:
     1.8 -  fixes y :: "'a::comm_ring_1"
     1.9 -  shows "(- numeral k) dvd y \<longleftrightarrow> (numeral k) dvd y"
    1.10 -  by (fact minus_dvd_iff)
    1.11 -
    1.12 -lemma dvd_neg_numeral_right [simp]:
    1.13 -  fixes x :: "'a::comm_ring_1"
    1.14 -  shows "x dvd (- numeral k) \<longleftrightarrow> x dvd (numeral k)"
    1.15 -  by (fact dvd_minus_iff)
    1.16 -
    1.17  lemmas dvd_eq_mod_eq_0_numeral [simp] =
    1.18    dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y
    1.19