proposition: Theorem Rolle' : (forall Ha Hb, F a Ha [=] F b Hb) -> forall e, [0] [<] e -> {x : IR | Compact Hab x | forall Hx, AbsIR (PartInt (ProjT1 HF) x Hx) [<=] e}.
proof: Proof. intros. unfold Hab in |- *. apply Rolle with F (diffble_imp_inc _ _ _ _ HF _ (compact_inc_lft a b Hab)) (diffble_imp_inc _ _ _ _ HF _ (compact_inc_rht a b Hab)). apply projT2. apply H. assumption. Qed.
imports: CoRN.tactics.DiffTactics2 CoRN.ftc.MoreFunctions