proposition: Lemma nondecreasing_fun_itv_partition a b f s : {in `[a, b] &, nondecreasing_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 <= F k.+1.
proof: Proof. move=> ndf abs F k ks. have [_] := nondecreasing_seqP F; apply => m n mn; rewrite /F/=. have [ms|ms] := ltnP m (size s).+1; last first. rewrite nth_default//. have [|ns] := ltnP n (size s).+1; last by rewrite nth_default. by move=> /(leq_ltn_trans mn); rewrite ltnS leqNgt ms. have [ns|ns] := ltnP n (size s).+1; last first. rewrite [in leRHS]nth_default//=; apply/ndf/itv_partition_nth_le => //. by rewrite in_itv/= itv_partition_nth_le// andbT itv_partition_nth_ge. by rewrite in_itv/= lexx andbT; exact: (itv_partition_le abs). move: abs; rewrite /itv_partition => -[] sa sab. move: mn; rewrite leq_eqVlt => /predU1P[->//|mn]. apply/ndf/ltW/sorted_ltn_nth => //=; last exact: lt_trans. by rewrite in_itv/= itv_partition_nth_le// andbT itv_partition_nth_ge. by rewrite in_itv/= itv_partition_nth_le// andbT itv_partition_nth_ge. 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)