proposition: Lemma ex_vitali_collection_partition i : V i -> exists n, vitali_collection_partition n i.
proof: Proof. move=> Vi; pose f := floor (r / (radius (B i))%:num). have f_ge0 : 0 <= f by rewrite floor_ge0// divr_ge0// ltW// (r_gt0 Vi). have [m /andP[mf fm]] := leq_ltn_expn `|f|.-1. exists m; split => //; apply/andP; split => [{mf}|{fm}]. rewrite -(@ler_nat R) in fm. rewrite ltr_pdivrMr// mulrC -ltr_pdivrMr// (lt_le_trans _ fm)//. rewrite (lt_le_trans (lt_succ_floor _))//= -/f -natr1 lerD2r//. have [<-|f0] := eqVneq 0 f; first by rewrite /= ler0n. rewrite prednK//; last by rewrite absz_gt0 eq_sym. by rewrite natr_absz// ger0_norm. move: m => [|m] in mf *; first by rewrite expn0 divr1 VBr. rewrite -(@ler_nat R) in mf. rewrite ler_pdivlMr// mulrC -ler_pdivlMr//. have [f0|f0] := eqVneq 0 f. by move: mf; rewrite -f0 absz0 leNgt expnS ltr_nat leq_pmulr// expn_gt0. rewrite (le_trans mf)// prednK//; last by rewrite absz_gt0 eq_sym. by rewrite natr_absz// ger0_norm// floor_le. 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