proposition: Lemma derive_increasing_interv : forall (a b:R) (f:R -> R) (pr:derivable f), a < b -> (forall t:R, a < t < b -> 0 < derive_pt f t (pr t)) -> forall x y:R, a <= x <= b -> a <= y <= b -> x < y -> f x < f y.
proof: Proof. intros. generalize (derive_increasing_interv_ax a b f pr H); intro. elim H4; intros H5 _; apply (H5 H0 x y H1 H2 H3). Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra