proposition: Lemma disjoint_vitali_collection_partition n m : n != m -> vitali_collection_partition n `&` vitali_collection_partition m = set0.
proof: Proof. move=> nm; wlog : n m nm / (n < m)%N. move=> wlg; move: nm; rewrite neq_lt => /orP[nm|mn]. by rewrite wlg// lt_eqF. by rewrite setIC wlg// lt_eqF. move=> {}nm; apply/seteqP; split => // i [] [Vi] /andP[rnB _] [_ /andP[_]]. move/(lt_le_trans rnB); rewrite ltr_pM2l//; last by rewrite (r_gt0 Vi). rewrite ltf_pV2 ?posrE ?ltr0n ?expn_gt0// ltr_nat. by move/ltn_pexp2l => /(_ isT); rewrite ltnNge => /negP; apply. 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