proposition: Lemma hlength_itv i : hlength [set` i] = if i.2 > i.1 then (i.2 : \bar R) - i.1 else 0.
proof: Proof. case: ltP => [/lt_ereal_bnd/neitvP i12|]; first by rewrite /hlength set_itvK. rewrite le_eqVlt => /orP[|/lt_ereal_bnd i12]; last first. rewrite (_ : [set` i] = set0) ?hlength0//. by apply/eqP/negPn; rewrite -/(neitv _) neitvE -leNgt (ltW i12). case: i => -[ba a|[|]] [bb b|[|]] //=. - rewrite /= => /eqP[->{b}]; move: ba bb => -[] []; try by rewrite set_itvE hlength0. by rewrite hlength_singleton. - by move=> _; rewrite set_itvE hlength0. - by move=> _; rewrite set_itvE hlength0. 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