proposition: Theorem derivable_neg_imp_decreasing : forall f f' dom, connected dom -> (forall x, dom x -> derivable_pt_lim f x (f' x) /\ (f' x <= 0)%R) -> forall u v, dom u -> dom v -> (u <= v)%R -> (f v <= f u)%R.
proof: Proof. intros f f' dom Hdom Hd u v Hu Hv Huv. apply Ropp_le_cancel. refine (derivable_pos_imp_increasing (opp_fct f) (opp_fct f') _ Hdom _ _ _ Hu Hv Huv). intros. destruct (Hd x H) as (H1, H2). split. apply derivable_pt_lim_opp with (1 := H1). rewrite <- Ropp_0. apply Ropp_le_contravar with (1 := H2). Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)