proposition: Lemma null_derivative_1 : forall (f:R -> R) (pr:derivable f), (forall x:R, derive_pt f x (pr x) = 0) -> constant f.
proof: Proof. intros. cut (forall x:R, derive_pt f x (pr x) <= 0). - cut (forall x:R, 0 <= derive_pt f x (pr x)). + intros. assert (H2 := nonneg_derivative_1 f pr H0). assert (H3 := nonpos_derivative_1 f pr H1). apply increasing_decreasing; assumption. + intro; right; symmetry ; apply (H x). - intro; right; apply (H x). Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra