proposition: Lemma nonincreasing_funN {R : realType} a b (f : R -> R) : {in `[a, b] &, nonincreasing_fun f} <-> {in `[a, b] &, nondecreasing_fun (\- f)}.
proof: Proof. apply: iff_sym; apply: (iff_trans (nondecreasing_funN a b (\- f))). rewrite [in X in _ <-> X](_ : f = \- (\- f))//. by apply/funext => x /=; rewrite opprK. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)