equal
deleted
inserted
replaced
127 apply (simp) |
127 apply (simp) |
128 apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))") |
128 apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))") |
129 apply (erule order_trans) |
129 apply (erule order_trans) |
130 apply (simp add: ring_distribs) |
130 apply (simp add: ring_distribs) |
131 apply (rule mult_left_mono) |
131 apply (rule mult_left_mono) |
132 apply assumption |
|
133 apply (simp add: order_less_le) |
|
134 apply (rule mult_left_mono) |
|
135 apply (simp add: abs_triangle_ineq) |
132 apply (simp add: abs_triangle_ineq) |
136 apply (simp add: order_less_le) |
133 apply (simp add: order_less_le) |
137 apply (rule mult_nonneg_nonneg) |
134 apply (rule mult_nonneg_nonneg) |
138 apply (rule add_nonneg_nonneg) |
135 apply (rule add_nonneg_nonneg) |
139 apply auto |
136 apply auto |
147 apply (erule order_trans) |
144 apply (erule order_trans) |
148 apply (simp) |
145 apply (simp) |
149 apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))") |
146 apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))") |
150 apply (erule order_trans) |
147 apply (erule order_trans) |
151 apply (simp add: ring_distribs) |
148 apply (simp add: ring_distribs) |
152 apply (rule mult_left_mono) |
|
153 apply (simp add: order_less_le) |
|
154 apply (simp add: order_less_le) |
|
155 apply (rule mult_left_mono) |
149 apply (rule mult_left_mono) |
156 apply (rule abs_triangle_ineq) |
150 apply (rule abs_triangle_ineq) |
157 apply (simp add: order_less_le) |
151 apply (simp add: order_less_le) |
158 apply (rule mult_nonneg_nonneg) |
152 apply (rule mult_nonneg_nonneg) |
159 apply (rule add_nonneg_nonneg) |
153 apply (rule add_nonneg_nonneg) |