proposition: Lemma derive_increasing_interv_ax : 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) /\ ((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. split; intros. - apply Rplus_lt_reg_l with (- f x). rewrite Rplus_opp_l; rewrite Rplus_comm. assert (H4 := MVT_cor1 f _ _ pr H3). elim H4; intros. elim H5; intros. unfold Rminus in H6. rewrite H6. apply Rmult_lt_0_compat. 2:{ lra. } apply H0. lra. - apply Rplus_le_reg_l with (- f x). rewrite Rplus_opp_l; rewrite Rplus_comm. assert (H4 := MVT_cor1 f _ _ pr H3). elim H4; intros. elim H5; intros. unfold Rminus in H6. rewrite H6. apply Rmult_le_pos. 2:{ lra. } apply H0. lra. Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra