proposition: Lemma nondecreasing_funN {R : realType} a b (f : R -> R) : {in `[a, b] &, nondecreasing_fun f} <-> {in `[a, b] &, nonincreasing_fun (\- f)}.
proof: Proof. split=> [h m n mab nab mn|h m n mab nab mn]; first by rewrite lerNr opprK h. by rewrite -(opprK (f n)) -lerNr h. 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)