proposition: Lemma nonneg_derivative_1 : forall (f:R -> R) (pr:derivable f), (forall x:R, 0 <= derive_pt f x (pr x)) -> increasing f.
proof: Proof. intros. unfold increasing. intros. destruct (total_order_T x y) as [[H1| ->]|H1]. - apply Rplus_le_reg_l with (- f x). rewrite Rplus_opp_l; rewrite Rplus_comm. pose proof (MVT_cor1 f _ _ pr H1) as (c & H3 & H4). unfold Rminus in H3. rewrite H3. apply Rmult_le_pos. + apply H. + apply Rplus_le_reg_l with x. rewrite Rplus_0_r; replace (x + (y + - x)) with y; [ assumption | ring ]. - right; reflexivity. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 H1)). Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra