Countable sums in ZF

[Timothy Y. Chow]

I was surprised to learn recently that the proof of "a positive 
real-valued function on [0,1] has a positive integral" requires countable 
choice (Kanovei and Katz, Real Analysis Exchange 42 (2017), 385-390).

Years ago, on MathOverflow, the following theorem was cited as being 
trickier to prove than it looks: If I_1, I_2, ... are intervals of real 
numbers with lengths that sum to less than 1, then their union cannot be 
all of [0,1].  Is there anything interesting about this theorem from a 
reverse mathematics perspective?

Tim