proposition: Lemma hlength_finite_fin_num i : neitv i -> hlength [set` i] < +oo -> ((i.1 : \bar R) \is a fin_num) /\ ((i.2 : \bar R) \is a fin_num).
proof: Proof. move: i => [[ba a|[]] [bb b|[]]] /neitvP //=; do ?by rewrite ?set_itvE ?eqxx. by move=> _; rewrite hlength_itv /= ltry. by move=> _; rewrite hlength_itv /= ltNyr. by move=> _; rewrite hlength_itv. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology numfun normedtype HB(structures) sequences esum measure real_interval realfun exp lebesgue_stieltjes_measure