proposition: Lemma positive_derivative : forall (f:R -> R) (pr:derivable f), (forall x:R, 0 < derive_pt f x (pr x)) -> strict_increasing f.
proof: Proof. intros. unfold strict_increasing. intros. apply Rplus_lt_reg_l with (- f x). rewrite Rplus_opp_l; rewrite Rplus_comm. assert (H1 := MVT_cor1 f _ _ pr H0). elim H1; intros. elim H2; intros. unfold Rminus in H3. rewrite H3. apply Rmult_lt_0_compat. - apply H. - apply Rplus_lt_reg_l with x. rewrite Rplus_0_r; replace (x + (y + - x)) with y; [ assumption | ring ]. Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra