proposition: Lemma wlength_finite_fin_num i : neitv i -> wlength [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 wlength_itv /= ltry. by move=> _; rewrite wlength_itv /= ltNye. by move=> _; rewrite wlength_itv. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) HB(structures) mathcomp.classical(mathcomp_extra boolp classical_sets) mathcomp.classical(functions fsbigop cardinality) reals ereal signed topology numfun normedtype sequences esum real_interval measure realfun