proposition: Lemma nonincreasing_fun_itv_partition a b f s : {in `[a, b] &, nonincreasing_fun f} -> itv_partition a b s -> let F : nat -> R := f \o nth b (a :: s) in forall k, (k < size s)%N -> F k.+1 <= F k.
proof: Proof. move/nonincreasing_funN => ndNf abs F k ks; rewrite -(opprK (F k)) lerNr. exact: (nondecreasing_fun_itv_partition ndNf abs). 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)