proposition: Theorem deriv_constant2 : forall f (a b c:R) (pr:derivable_pt f c), a < c -> c < b -> (forall x:R, a < x -> x < b -> f x = f c) -> derive_pt f c pr = 0.
proof: Proof. intros. eapply deriv_maximum with a b; try assumption. intros; right; apply (H1 x H2 H3). Qed.
imports: Rbase Rfunctions Rlimit Rderiv