proposition: Lemma derive1_at_min (R : realFieldType) (f : R -> R) (a b c : R) : a <= b -> (forall t, t \in `]a, b[%R -> derivable f t 1) -> c \in `]a, b[%R -> (forall t, t \in `]a, b[%R -> f c <= f t) -> is_derive c 1 f 0.
proof: Proof. move=> leab fdrvbl cab cmin; apply: DeriveDef; first exact: fdrvbl. apply/eqP; rewrite -oppr_eq0; apply/eqP. rewrite -deriveN; last exact: fdrvbl. suff df : is_derive c 1 (- f) 0 by rewrite derive_val. apply: derive1_at_max leab _ (cab) _ => t tab; first exact/derivableN/fdrvbl. by rewrite lerN2; apply: cmin. 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