src/HOL/Library/Convex.thy
 changeset 56536 aefb4a8da31f parent 56479 91958d4b30f7 child 56541 0e3abadbef39
1.1 --- a/src/HOL/Library/Convex.thy	Fri Apr 11 12:43:22 2014 +0200
1.2 +++ b/src/HOL/Library/Convex.thy	Fri Apr 11 13:36:57 2014 +0200
1.3 @@ -606,7 +606,7 @@
1.4      have "z3 \<in> C" using z3 asm atMostAtLeast_subset_convex
1.5        `convex C` `x \<in> C` `z1 \<in> C` `x < z1` by fastforce
1.6      then have B': "f'' z3 \<ge> 0" using assms by auto
1.7 -    from A' B' have "(y - z1) * f'' z3 \<ge> 0" using mult_nonneg_nonneg by auto
1.8 +    from A' B' have "(y - z1) * f'' z3 \<ge> 0" by auto
1.9      from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0" by auto
1.10      from mult_right_mono_neg[OF this le(2)]
1.11      have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \<le> 0 * (x - y)"
1.12 @@ -621,7 +621,7 @@
1.13      have "z2 \<in> C" using z2 z1 asm atMostAtLeast_subset_convex
1.14        `convex C` `z1 \<in> C` `y \<in> C` `z1 < y` by fastforce
1.15      then have B: "f'' z2 \<ge> 0" using assms by auto
1.16 -    from A B have "(z1 - x) * f'' z2 \<ge> 0" using mult_nonneg_nonneg by auto
1.17 +    from A B have "(z1 - x) * f'' z2 \<ge> 0" by auto
1.18      from cool this have "(f y - f x) / (y - x) - f' x \<ge> 0" by auto
1.19      from mult_right_mono[OF this ge(2)]
1.20      have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \<ge> 0 * (y - x)"