proposition: Lemma le0r_derive1_ndecr (R : realType) (f : R -> R) (a b : R) : (forall x, x \in `]a, b[%R -> derivable f x 1) -> (forall x, x \in `]a, b[%R -> 0 <= f^`() x) -> {within `[a,b], continuous f} -> forall x y, a <= x -> x <= y -> y <= b -> f x <= f y.
proof: Proof. move=> fdrvbl dfge0 fcont x y; rewrite -[f _ <= _]lerN2. apply (@ler0_derive1_nincr _ (- f)) => t tab; first exact/derivableN/fdrvbl. rewrite derive1E deriveN; last exact: fdrvbl. by rewrite oppr_le0 -derive1E; apply: dfge0. by apply: continuousN; exact: fcont. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms