proposition: Lemma MVT_segment (R : realType) (f df : R -> R) (a b : R) : a <= b -> (forall x, x \in `]a, b[%R -> is_derive x 1 f (df x)) -> {within `[a, b], continuous f} -> exists2 c, c \in `[a, b]%R & f b - f a = df c * (b - a).
proof: Proof. move=> leab fdrvbl fcont; case: ltgtP leab => // [altb|aeb]; last first. by exists a; [rewrite inE/= aeb lexx|rewrite aeb !subrr mulr0]. have [c cab D] := MVT altb fdrvbl fcont. by exists c => //; rewrite in_itv /= ltW (itvP cab). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms