# HG changeset patch
# User Andreas Lochbihler
# Date 1447232889 -3600
# Node ID ec580491c5d27f0f72b48873902514f1bd0ea773
# Parent  4f7ef088c4eddba1a6734b85eb5b3a3fbb893dba
generalise lemma

diff -r 4f7ef088c4ed -r ec580491c5d2 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Nov 11 10:07:27 2015 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Nov 11 10:08:09 2015 +0100
@@ -1161,13 +1161,8 @@
   unfolding mult.commute[of _ c] nn_integral_cmult[OF assms] by simp
 
 lemma nn_integral_divide:
-  "0 < c \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> (\<integral>\<^sup>+x. f x / c \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M) / c"
-  unfolding divide_ereal_def
-  apply (rule nn_integral_multc)
-  apply assumption
-  apply (cases c)
-  apply auto
-  done
+   "\<lbrakk> 0 \<le> c; f \<in> borel_measurable M \<rbrakk> \<Longrightarrow> (\<integral>\<^sup>+ x. f x / c \<partial>M) = (\<integral>\<^sup>+ x. f x \<partial>M) / c"
+by(simp add: divide_ereal_def nn_integral_multc inverse_ereal_ge0I)
 
 lemma nn_integral_indicator[simp]:
   "A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x. indicator A x\<partial>M) = (emeasure M) A"