exists_volume_slice_lt_eps

lemma exists_volume_slice_lt_eps {ε : ℝ≥0∞} (εpos : 0 < ε) :    ∃ n, volume (slice CP bG mG (n + 1)).G < ε := by  suffices ∃ n, 2⁻¹ ^ (n + 1) * volume G < ε by    obtain ⟨n, hn⟩ := this    exact ⟨n, volume_slice_le_inv_two_pow_mul.trans_lt hn⟩  rcases eq_zero_or_pos (volume G) with vG | vG; · simpa [vG]  have vGnt : volume G ≠ ⊤ := bG.measure_lt_top.ne  conv =>    enter [1, n]    rw [← ENNReal.lt_div_iff_mul_lt (.inl vG.ne') (.inl vGnt), pow_succ', ← ENNReal.div_eq_inv_mul,      ENNReal.div_lt_iff (.inl two_ne_zero) (.inl ofNat_ne_top)]  have εdvn0 : ε / volume G * 2 ≠ 0 :=    mul_ne_zero (ENNReal.div_ne_zero.mpr ⟨εpos.ne', vGnt⟩) two_ne_zero  exact exists_inv_two_pow_lt εdvn0