src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy

--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Apr 14 13:08:17 2014 +0200
@@ -64,11 +64,6 @@
   apply auto
   done
 
-lemma divide_nonneg_nonneg:
-  fixes a b :: "'a :: {linordered_field, field_inverse_zero}"
-  shows "a \<ge> 0 \<Longrightarrow> b \<ge> 0 \<Longrightarrow> 0 \<le> a / b"
-  by (cases "b = 0") (auto intro!: divide_nonneg_pos)
-
 lemma setsum_Un_disjoint':
   assumes "finite A"
     and "finite B"