proposition: Lemma finite_hlength_itv i : neitv i -> hlength [set` i] < +oo -> hlength [set` i] = (fine i.2)%:E - (fine i.1)%:E.
proof: Proof. move=> i0 ioo; have [ri1 ri2] := hlength_finite_fin_num i0 ioo. rewrite !fineK// hlength_itv; case: ifPn => //. rewrite -leNgt le_eqVlt => /predU1P[->|]; first by rewrite subee. by move/lt_ereal_bnd/ltW; rewrite leNgt; move: i0 => /neitvP => ->. 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