proposition: Lemma bounded_variation_pos_neg_tvE a b f : BV a b f -> {in `[a, b], f =1 (fine \o pos_tv a f) \- (fine \o neg_tv a f)}.
proof: Proof. move=> bdabf x; rewrite in_itv /= => /andP [ax xb]. have ffin: TV a x f \is a fin_num. apply/bounded_variationP => //. exact: (bounded_variationl _ xb). have Nffin : TV a x (\- f) \is a fin_num. apply/bounded_variationP => //; apply/bounded_variationN. exact: (bounded_variationl ax xb). rewrite /pos_tv /neg_tv /= total_variationN -fineB -?muleBl // ?fineM //. - rewrite addeAC oppeD //= ?fin_num_adde_defl //. by rewrite addeA subee // add0e -EFinD //= opprK mulrDl -Num.Theory.splitr. - by rewrite fin_numB ?fin_numD ?ffin; apply/andP; split. - by apply: fin_num_adde_defl; rewrite fin_numN fin_numD; apply/andP; split. - by rewrite fin_numM // fin_numD; apply/andP; split. - by rewrite fin_numM // fin_numD; apply/andP; split. 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)