proposition: Lemma nonneg_derivative_0 : forall f (pr:derivable f), increasing f -> forall x:R, 0 <= derive_pt f x (pr x).
proof: Proof. intros; unfold increasing in H. assert (H0 := derivable_derive f x (pr x)). elim H0; intros l H1. rewrite H1; case (Rtotal_order 0 l); intro. - left; assumption. - elim H2; intro. + right; assumption. + assert (H4 := derive_pt_eq_1 f x l (pr x) H1). cut (0 < - (l / 2)). 1:intro; elim (H4 (- (l / 2)) H5); intros delta H6. 1:cut (delta / 2 <> 0 /\ 0 < delta / 2 /\ Rabs (delta / 2) < delta). 1:intro; decompose [and] H7; intros; generalize (H6 (delta / 2) H8 H11); cut (0 <= (f (x + delta / 2) - f x) / (delta / 2)). 1:intro; cut (0 <= (f (x + delta / 2) - f x) / (delta / 2) - l). * intro; unfold Rabs; case (Rcase_abs ((f (x + delta / 2) - f x) / (delta / 2) - l)) as [Hlt|Hge]. -- elim (Rlt_irrefl 0 (Rle_lt_trans 0 ((f (x + delta / 2) - f x) / (delta / 2) - l) 0 H12 Hlt)). -- intros; generalize (Rplus_lt_compat_r l ((f (x + delta / 2) - f x) / (delta / 2) - l) (- (l / 2)) H13); unfold Rminus; replace (- (l / 2) + l) with (l / 2). ++ rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; intro; generalize (Rle_lt_trans 0 ((f (x + delta / 2) - f x) / (delta / 2)) (l / 2) H9 H14); intro; cut (l / 2 < 0). ** intro; elim (Rlt_irrefl 0 (Rlt_trans 0 (l / 2) 0 H15 H16)). ** rewrite <- Ropp_0 in H5; generalize (Ropp_lt_gt_contravar (-0) (- (l / 2)) H5); repeat rewrite Ropp_involutive; intro; assumption. ++ pattern l at 3; rewrite <-Rplus_half_diag. ring. * unfold Rminus; apply Rplus_le_le_0_compat. -- unfold Rdiv; apply Rmult_le_pos. ++ cut (x <= x + delta * / 2). ** intro; generalize (H x (x + delta * / 2) H12); intro; generalize (Rplus_le_compat_l (- f x) (f x) (f (x + delta * / 2)) H13); rewrite Rplus_opp_l; rewrite Rplus_comm; intro; assumption. ** pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l; left; assumption. ++ left; apply Rinv_0_lt_compat; assumption. -- left; rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; assumption. * unfold Rdiv; apply Rmult_le_pos. -- cut (x <= x + delta * / 2). ++ intro; generalize (H x (x + delta * / 2) H9); intro; generalize (Rplus_le_compat_l (- f x) (f x) (f (x + delta * / 2)) H12); rewrite Rplus_opp_l; rewrite Rplus_comm; intro; assumption. ++ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l; left; assumption. -- left; apply Rinv_0_lt_compat; assumption. * split. -- unfold Rdiv; apply prod_neq_R0. ++ generalize (cond_pos delta); intro; red; intro H9; rewrite H9 in H7; elim (Rlt_irrefl 0 H7). ++ apply Rinv_neq_0_compat; discrR. -- split. ++ unfold Rdiv; apply Rmult_lt_0_compat; [ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ]. ++ replace (Rabs (delta / 2)) with (delta / 2). ** unfold Rdiv; apply Rmult_lt_reg_l with 2. { prove_sup0. } rewrite (Rmult_comm 2). rewrite Rmult_assoc; rewrite Rinv_l; [ idtac | discrR ]. rewrite Rmult_1_r. rewrite <-Rplus_diag. pattern (pos delta) at 1; rewrite <- Rplus_0_r. apply Rplus_lt_compat_l; apply (cond_pos delta). ** symmetry ; apply Rabs_right. left; change (0 < delta / 2); unfold Rdiv; apply Rmult_lt_0_compat; [ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ]. * unfold Rdiv; rewrite <- Ropp_mult_distr_l_reverse; apply Rmult_lt_0_compat. -- apply Rplus_lt_reg_l with l. unfold Rminus; rewrite Rplus_opp_r; rewrite Rplus_0_r; assumption. -- apply Rinv_0_lt_compat; prove_sup0. Qed.
imports: Rbase Rfunctions Rlimit Rderiv