proposition: Theorem deriv_minimum : forall f (a b c:R) (pr:derivable_pt f c), a < c -> c < b -> (forall x:R, a < x -> x < b -> f c <= f x) -> derive_pt f c pr = 0.
proof: Proof. intros. rewrite <- (Ropp_involutive (derive_pt f c pr)). apply Ropp_eq_0_compat. rewrite <- (derive_pt_opp f c pr). cut (forall x:R, a < x -> x < b -> (- f)%F x <= (- f)%F c). - intro. apply (deriv_maximum (- f)%F a b c (derivable_pt_opp _ _ pr) H H0 H2). - intros; unfold opp_fct; apply Ropp_ge_le_contravar; apply Rle_ge. apply (H1 x H2 H3). Qed.
imports: Rbase Rfunctions Rlimit Rderiv