proposition: Lemma incr_function (f : R -> R) (a b : Rbar) (df : R -> R) : (forall (x : R), Rbar_lt a x -> Rbar_lt x b -> is_derive f x (df x)) -> ((forall (x : R), Rbar_lt a x -> Rbar_lt x b -> df x > 0) -> (forall (x y : R), Rbar_lt a x -> x < y -> Rbar_lt y b -> f x < f y)).
proof: Proof. move => Df Hf x y Hax Hxy Hyb. apply Rminus_lt_0. case: (MVT_gen f x y df) => [z Hz | z Hz | c [Hc ->]]. apply Df. apply Rbar_lt_le_trans with (y := Rmin x y) (2 := Rlt_le _ _ (proj1 Hz)). rewrite /Rmin ; case: Rle_dec (Rlt_le _ _ Hxy) => //. apply Rbar_le_lt_trans with (y := Rmax x y) (1 := Rlt_le _ _ (proj2 Hz)). rewrite /Rmax ; case: Rle_dec (Rlt_le _ _ Hxy) => //. apply derivable_continuous_pt. exists (df z) ; apply is_derive_Reals, Df. apply Rbar_lt_le_trans with (y := Rmin x y) (2 := proj1 Hz). rewrite /Rmin ; case: Rle_dec (Rlt_le _ _ Hxy) => //. apply Rbar_le_lt_trans with (y := Rmax x y) (1 := proj2 Hz). rewrite /Rmax ; case: Rle_dec (Rlt_le _ _ Hxy) => //. apply Rmult_lt_0_compat. apply Hf. apply Rbar_lt_le_trans with (y := Rmin x y) (2 := proj1 Hc). rewrite /Rmin ; case: Rle_dec (Rlt_le _ _ Hxy) => //. apply Rbar_le_lt_trans with (y := Rmax x y) (1 := proj2 Hc). rewrite /Rmax ; case: Rle_dec (Rlt_le _ _ Hxy) => //. by apply -> Rminus_lt_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv