proposition: Lemma ler0_derive1_nincr (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 -> f^`() x <= 0) -> {within `[a,b], continuous f} -> forall x y, a <= x -> x <= y -> y <= b -> f y <= f x.
proof: Proof. move=> fdrvbl dfle0 ctsf x y leax lexy leyb; rewrite -subr_ge0. case: ltgtP lexy => // [xlty|->]; last by rewrite subrr. have itvW : {subset `[x, y]%R <= `[a, b]%R}. by apply/subitvP; rewrite /<=%O /= /<=%O /= leyb leax. have itvWlt : {subset `]x, y[%R <= `]a, b[%R}. by apply subitvP; rewrite /<=%O /= /<=%O /= leyb leax. have fdrv z : z \in `]x, y[%R -> is_derive z 1 f (f^`()z). rewrite in_itv/= => /andP[xz zy]; apply: DeriveDef; last by rewrite derive1E. by apply: fdrvbl; rewrite in_itv/= (le_lt_trans _ xz)// (lt_le_trans zy). have [] := @MVT _ f (f^`()) x y xlty fdrv. apply: (@continuous_subspaceW _ _ _ `[a,b]); first exact: itvW. by rewrite continuous_subspace_in. move=> t /itvWlt dft dftxy _; rewrite -oppr_le0 opprB dftxy. by apply: mulr_le0_ge0 => //; [exact: dfle0|by rewrite subr_ge0 ltW]. 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