src/HOL/Fields.thy
changeset 56414 c1bbd3e22226
parent 56410 a14831ac3023
child 56441 49e95c9ebb59
equal deleted inserted replaced
56413:2d4d9a5f68ff 56414:c1bbd3e22226
   410 
   410 
   411 lemma divide_minus_right [field_simps]:
   411 lemma divide_minus_right [field_simps]:
   412   "a / - b = - (a / b)"
   412   "a / - b = - (a / b)"
   413   by (simp add: divide_inverse)
   413   by (simp add: divide_inverse)
   414 
   414 
   415 lemma minus_divide_divide:
   415 lemma minus_divide_divide [simp]:
   416   "(- a) / (- b) = a / b"
   416   "(- a) / (- b) = a / b"
   417 apply (cases "b=0", simp) 
   417 apply (cases "b=0", simp) 
   418 apply (simp add: nonzero_minus_divide_divide) 
   418 apply (simp add: nonzero_minus_divide_divide) 
   419 done
   419 done
   420 
   420