proposition: Lemma bounded_variationP a b f : a <= b -> BV a b f <-> TV a b f \is a fin_num.
proof: Proof. rewrite le_eqVlt => /predU1P[<-{b}|ab]. by rewrite total_variationxx; split => // ?; exact: bounded_variationxx. rewrite ge0_fin_numE; last exact/total_variation_ge0/ltW. split=> [abf|]. by rewrite /total_variation ereal_sup_EFin ?ltry//; exact: variations_neq0. rewrite /total_variation /bounded_variation ltey => /eqP; apply: contra_notP. by move/hasNub_ereal_sup; apply; exact: variations_neq0. 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)