proposition: Lemma negative_derivative : forall (f:R -> R) (pr:derivable f), (forall x:R, derive_pt f x (pr x) < 0) -> strict_decreasing f.
proof: Proof. intros. assert (forall h:R, - - f h = f h) by (intros;ring). generalize (strictincreasing_strictdecreasing_opp (- f)%F). unfold strict_decreasing, opp_fct. intros. rewrite <- (H0 x). rewrite <- (H0 y). apply H1; [ idtac | assumption ]. cut (forall x:R, 0 < derive_pt (- f) x (derivable_opp f pr x)). { intros; eapply positive_derivative; apply H3. } 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_lt_gt_contravar; apply (H x0). Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra