proposition: Lemma nonpos_derivative_1 : forall (f:R -> R) (pr:derivable f), (forall x:R, derive_pt f x (pr x) <= 0) -> decreasing f.
proof: Proof. intros. assert (forall h:R, - - f h = f h) by (intros;ring). generalize (increasing_decreasing_opp (- f)%F). unfold decreasing. unfold opp_fct. intros. rewrite <- (H0 x); rewrite <- (H0 y). apply H1. 2:{ assumption. } assert (forall x:R, 0 <= derive_pt (- f) x (derivable_opp f pr x)). { intro. assert (H3 := derive_pt_opp f x0 (pr x0)). assert (derive_pt (- f) x0 (derivable_pt_opp f x0 (pr x0)) = derive_pt (- f) x0 (derivable_opp f pr x0)) by apply pr_nu. rewrite <- H4. rewrite H3. rewrite <- Ropp_0; apply Ropp_ge_le_contravar; apply Rle_ge; apply (H x0). } replace (fun x:R => - f x) with (- f)%F; [ idtac | reflexivity ]. apply (nonneg_derivative_1 (- f)%F (derivable_opp f pr) H3). Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra