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)"