proposition: Lemma nonpos_derivative_0 : forall (f:R -> R) (pr:derivable f), decreasing f -> forall x:R, derive_pt f x (pr x) <= 0.
proof: Proof. intros f pr H x; assert (H0 := H); unfold decreasing in H0; generalize (derivable_derive f x (pr x)); intro; elim H1; intros l H2. rewrite H2; case (Rtotal_order l 0); intro. { left; assumption. } elim H3; intro. { right; assumption. } generalize (derive_pt_eq_1 f x l (pr x) H2); intros; assert (0 < l / 2). { unfold Rdiv; apply Rmult_lt_0_compat; [ apply H4 | apply Rinv_0_lt_compat; prove_sup0 ]. } elim (H5 (l / 2) H6); intros delta H7; assert (delta / 2 <> 0 /\ 0 < delta / 2 /\ Rabs (delta / 2) < delta). { split;[|split]. - unfold Rdiv; apply prod_neq_R0. + generalize (cond_pos delta); intro; red; intro H9; rewrite H9 in H8; elim (Rlt_irrefl 0 H8). + apply Rinv_neq_0_compat; discrR. - unfold Rdiv; destruct delta;simpl; lra. - rewrite Rabs_right. + unfold Rdiv; apply Rmult_lt_reg_l with 2. { prove_sup0. } rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite Rinv_r. 2:{ discrR. } rewrite Rmult_1_l; rewrite <-Rplus_diag; pattern (pos delta) at 1; rewrite <- Rplus_0_r. apply Rplus_lt_compat_l; apply (cond_pos delta). + apply Rle_ge; unfold Rdiv; left; apply Rmult_lt_0_compat. * apply (cond_pos delta). * apply Rinv_0_lt_compat; prove_sup0. } decompose [and] H8; intros; generalize (H7 (delta / 2) H9 H12); assert ((f (x + delta / 2) - f x) / (delta / 2) <= 0). { replace ((f (x + delta / 2) - f x) / (delta / 2)) with (- ((f x - f (x + delta / 2)) / (delta / 2))). - rewrite <- Ropp_0. apply Ropp_ge_le_contravar. apply Rle_ge. unfold Rdiv; apply Rmult_le_pos. + cut (x <= x + delta * / 2). * intro; generalize (H0 x (x + delta * / 2) H10); intro. generalize (Rplus_le_compat_l (- f (x + delta / 2)) (f (x + delta / 2)) (f x) 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. - unfold Rdiv; rewrite <- Ropp_mult_distr_l_reverse. rewrite Ropp_minus_distr. reflexivity. } assert (0 < - ((f (x + delta / 2) - f x) / (delta / 2) - l)) by lra. unfold Rabs; case (Rcase_abs ((f (x + delta / 2) - f x) / (delta / 2) - l)) as [Hlt|Hge]; lra. Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra