src/HOL/Analysis/Ball_Volume.thy
changeset 67719 bffb7482faaa
parent 67399 eab6ce8368fa
child 67976 75b94eb58c3d
     1.1 --- a/src/HOL/Analysis/Ball_Volume.thy	Sat Feb 24 17:21:35 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Ball_Volume.thy	Sun Feb 25 12:54:55 2018 +0000
     1.3 @@ -17,8 +17,11 @@
     1.4  definition unit_ball_vol :: "real \<Rightarrow> real" where
     1.5    "unit_ball_vol n = pi powr (n / 2) / Gamma (n / 2 + 1)"
     1.6  
     1.7 +lemma unit_ball_vol_pos [simp]: "n \<ge> 0 \<Longrightarrow> unit_ball_vol n > 0"
     1.8 +  by (force simp: unit_ball_vol_def intro: divide_nonneg_pos)
     1.9 +
    1.10  lemma unit_ball_vol_nonneg [simp]: "n \<ge> 0 \<Longrightarrow> unit_ball_vol n \<ge> 0"
    1.11 -  by (auto simp add: unit_ball_vol_def intro!: divide_nonneg_pos Gamma_real_pos)
    1.12 +  by (simp add: dual_order.strict_implies_order)
    1.13  
    1.14  text \<open>
    1.15    We first need the value of the following integral, which is at the core of