proposition: Lemma MVT_cor4: forall (f df : R -> R) a eps, (forall c, Rabs (c - a) <= eps -> is_derive f c (df c)) -> forall b, (Rabs (b - a) <= eps) -> exists c, f b - f a = df c * (b - a) /\ (Rabs (c - a) <= Rabs (b - a)).
proof: Proof. intros f df a eps Hf' b. unfold Rabs at 1 3. case Rcase_abs; intros H1 H2. destruct (MVT_cor2 f df b a). rewrite -(Rplus_0_l a). now apply Rlt_minus_l. intros c Hc. apply is_derive_Reals, Hf'. rewrite Rabs_left1. apply Rle_trans with (2:=H2). apply Ropp_le_contravar. now apply Rplus_le_compat_r. apply Rplus_le_reg_r with a. now ring_simplify. exists x; split. rewrite -RIneq.Ropp_minus_distr (proj1 H). ring. rewrite Rabs_left. apply Ropp_le_contravar. left; now apply Rplus_lt_compat_r. apply Rplus_lt_reg_r with a. now ring_simplify. destruct H1. destruct (MVT_cor2 f df a b). apply Rplus_lt_reg_r with (-a). ring_simplify. now rewrite Rplus_comm. intros c Hc. apply is_derive_Reals, Hf'. rewrite Rabs_right. apply Rle_trans with (2:=H2). now apply Rplus_le_compat_r. apply Rle_ge; apply Rplus_le_reg_r with a. now ring_simplify. exists x; split. exact (proj1 H0). rewrite Rabs_right. left; now apply Rplus_lt_compat_r. apply Rle_ge; apply Rplus_le_reg_r with a. left; now ring_simplify. exists a. replace b with a. split;[ring|idtac]. rewrite /Rminus Rplus_opp_r Rabs_R0. apply Rle_refl. apply Rplus_eq_reg_l with (-a). ring_simplify. rewrite - H; ring. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv