proposition: Lemma vitali_lemma_finite_cover (s : seq I) : { D : seq I | [/\ uniq D, {subset D <= s}, trivIset [set` D] B & cover [set` s] B `<=` cover [set` D] (scale_ball 3%:R \o B)] }.
proof: Proof. have [D [uD DV tD maxD]] := vitali_lemma_finite s. exists D; split => // x [i Vi] cBix/=. by have [j [Dj BiBj ij]] := maxD i Vi; move/(_ _ cBix) => ?; exists j. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule