I did finally write up that covering argument in Haskell, the core of it is

vitali :: [Ball] -> [Ball]

vitali [] = []

vitali balls =

let b = maximumBy (compare `on` radius) balls

newBalls = filter (not . intersects b) balls

in b : vitali newBalls

(the significance is that you can show that the new collection of balls here is disjoint and has total volume ≥ 1/3ᵈ times the total volume of the original collection.)