proposition: Lemma hlength_sigma_finite : sigma_finite setT (hlength : set (ocitv_type R) -> _).
proof: Proof. exists (fun k : nat => `] (- k%:R)%R, k%:R]%classic); first by rewrite bigcup_itvT. by move=> k; split => //; rewrite hlength_itv/= -EFinB; case: ifP; rewrite ltry. 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