proposition: Theorem Law_of_the_Mean_Abs_ineq : forall a b, I a -> I b -> forall c, (forall x, Compact (Min_leEq_Max a b) x -> forall Hx, AbsIR (F' x Hx) [<=] c) -> forall Ha Hb, AbsIR (F b Hb[-]F a Ha) [<=] c[*]AbsIR (b[-]a).
proof: Proof. intros a b Ia Ib c Hc Ha Hb. astepr (c[*]AbsIR (b[-]a) [+][0]). apply shift_leEq_plus'. apply approach_zero_weak. intros e H. elim Law_of_the_Mean with a b e; auto. intros x H0 H1. cut (Dom F' x). intro H2. eapply leEq_transitive. 2: apply (H1 Ha Hb H2). eapply leEq_transitive. 2: apply triangle_IR_minus'. unfold cg_minus at 1 4 in |- *; apply plus_resp_leEq_lft. apply inv_resp_leEq. stepl (AbsIR (F' x H2)[*]AbsIR(b[-]a)). 2:apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply mult_resp_leEq_rht. auto. apply AbsIR_nonneg. apply (Derivative_imp_inc' _ _ _ _ derF). exact (included_interval I a b Ia Ib (Min_leEq_Max a b) x H0). Qed.
imports: CoRN.tactics.DiffTactics2 CoRN.ftc.MoreFunctions