proposition: Lemma kzero_uub : measure_fam_uub kzero.
proof: Proof. by exists 1%R => /= t; rewrite /mzero/=. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology normedtype sequences esum measure numfun lebesgue_measure lebesgue_integral