proposition: Lemma fine_neg_tv_nondecreasing a b f : BV a b f -> {in `[a, b] &, nondecreasing_fun (fine \o neg_tv a f)}.
proof: Proof. move=> bdv p q pab qab pq /=. move: (pab) (qab); rewrite ?in_itv /= => /andP[ap pb] /andP[aq qb]. apply: fine_le; rewrite /neg_tv ?fin_numM // ?fin_numB /=. - apply/andP; split => //; apply/bounded_variationP => //. exact: (bounded_variationl _ pb). - apply/andP; split => //; apply/bounded_variationP => //. exact: (bounded_variationl _ qb). exact: (neg_tv_nondecreasing _ pab). 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)