proposition: Theorem Law_of_the_Mean_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, F b Hb[-]F a Ha [<=] c[*]AbsIR (b[-]a).
proof: Proof. intros. eapply leEq_transitive. apply leEq_AbsIR. apply Law_of_the_Mean_Abs_ineq; assumption. Qed.
imports: CoRN.tactics.DiffTactics2 CoRN.ftc.MoreFunctions