src/HOL/Library/Convex.thy
 changeset 56571 f4635657d66f parent 56544 b60d5d119489 child 56796 9f84219715a7
```     1.1 --- a/src/HOL/Library/Convex.thy	Mon Apr 14 10:55:56 2014 +0200
1.2 +++ b/src/HOL/Library/Convex.thy	Mon Apr 14 13:08:17 2014 +0200
1.3 @@ -138,7 +138,7 @@
1.4      with `0 \<le> setsum a s` have "0 < setsum a s" by simp
1.5      then have "(\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C"
1.6        using `\<forall>j\<in>s. 0 \<le> a j` and `\<forall>j\<in>s. y j \<in> C`
1.7 -      by (simp add: IH divide_nonneg_pos setsum_divide_distrib [symmetric])
1.8 +      by (simp add: IH setsum_divide_distrib [symmetric])
1.9      from `convex C` and `y i \<in> C` and this and `0 \<le> a i`
1.10        and `0 \<le> setsum a s` and `a i + setsum a s = 1`
1.11      have "a i *\<^sub>R y i + setsum a s *\<^sub>R (\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C"
1.12 @@ -432,9 +432,7 @@
1.13      then have "a i < 1" using asm by auto
1.14      then have i0: "1 - a i > 0" by auto
1.15      let ?a = "\<lambda>j. a j / (1 - a i)"
1.16 -    { fix j assume "j \<in> s"
1.17 -      then have "?a j \<ge> 0"
1.18 -        using i0 asms divide_nonneg_pos
1.19 +    { fix j assume "j \<in> s" with i0 asms have "?a j \<ge> 0"
1.20          by fastforce }
1.21      note a_nonneg = this
1.22      have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
```