proposition: Lemma Law_of_the_Mean'_I : forall HA HB e, [0] [<] e -> {x : IR | Compact Hab x | forall Hx, AbsIR (F b HB[-]F a HA[-]PartInt (ProjT1 HF) x Hx[*] (b[-]a)) [<=] e}.
proof: Proof. intros. unfold Hab in |- *. apply Law_of_the_Mean_I. apply projT2. assumption. Qed.
imports: CoRN.tactics.DiffTactics2 CoRN.ftc.MoreFunctions