proposition: Lemma bounded_variation (h dh : R -> R) (D : R) (x y : R) : (forall t : R, Rabs (t - x) <= Rabs (y - x) -> is_derive h t (dh t) /\ (Rabs (dh t) <= D)) -> Rabs (h y - h x) <= D * Rabs (y - x).
proof: Proof. intros H. destruct (MVT_cor4 h dh x (Rabs (y - x))) with (b := y) as [t Ht]. intros c Hc. specialize (H c Hc). apply H. apply Rle_refl. rewrite (proj1 Ht). rewrite Rabs_mult. apply Rmult_le_compat_r. apply Rabs_pos. now apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv