proposition: Lemma FConst_prop : forall J pJ F', Derivative J pJ F' [-C-][0] -> {c : IR | Feq J F' [-C-]c}.
proof: Proof. intros J pJ F' H. elim (nonvoid_point _ (proper_nonvoid _ pJ)); intros x0 Hx0. exists (F' x0 (Derivative_imp_inc _ _ _ _ H x0 Hx0)). FEQ. rename X into H0. simpl in |- *. apply cg_inv_unique_2. apply AbsIR_approach_zero; intros e H1. simpl in Hx'. elim (Law_of_the_Mean _ _ _ _ H _ _ Hx0 H0 e H1). intros y H2 H3. eapply leEq_wdl. apply (H3 (Derivative_imp_inc _ _ _ _ H _ Hx0) Hx I). apply AbsIR_wd; simpl in |- *; rational. Qed.
imports: CoRN.ftc.Rolle CoRN.tactics.DiffTactics3