src/HOL/Divides.thy
changeset 60516 0826b7025d07
parent 60429 d3d1e185cd63
child 60517 f16e4fb20652
     1.1 --- a/src/HOL/Divides.thy	Fri Jun 19 15:55:22 2015 +0200
     1.2 +++ b/src/HOL/Divides.thy	Fri Jun 19 07:53:33 2015 +0200
     1.3 @@ -131,9 +131,6 @@
     1.4  lemma mod_self [simp]: "a mod a = 0"
     1.5    using mod_mult_self2_is_0 [of 1] by simp
     1.6  
     1.7 -lemma div_self [simp]: "a \<noteq> 0 \<Longrightarrow> a div a = 1"
     1.8 -  using div_mult_self2_is_id [of _ 1] by simp
     1.9 -
    1.10  lemma div_add_self1 [simp]:
    1.11    assumes "b \<noteq> 0"
    1.12    shows "(b + a) div b = a div b + 1"