Lean ℝ≥0∞ binary expansions: avoid subtraction with a 'partial sum + room' lemma

For x = ∑' i, bitw (X i) i (bitw b i = if b then (1/2)^(i+1) else 0) in ℝ≥0∞, the strict bounds S_m < x < S_m + 2^{-m} (S_m = partial sum, needed when proving x non-dyadic) come cleanly without ENNReal subtraction. (1) Monotone lemma: m ≤ k → S_k + (1/2)^k ≤ S_m + (1/2)^m, by induction on m ≤ k using (1/2)^k = (1/2)^(k+1) + (1/2)^(k+1). (2) A later 0 at k gives x ≤ S_{k+1} + (1/2)^(k+1) and S_{k+1} = S_k, so x + (1/2)^(k+1) ≤ S_m + (1/2)^m. Conclude with ENNReal.lt_add_right (x ≠ ⊤). (3) A later 1 gives S_m + (1/2)^(k+1) ≤ S_{k+1} ≤ x. Tail bound: Summable.sum_add_tsum_nat_add' with ENNReal.summable, then ENNReal.tsum_geometric and ENNReal.one_sub_inv_two. To compare dyadics a·2^{-p} vs b·2^{-q} with natural a, b, multiply by 2^p·2^q via ENNReal.mul_le_mul_iff_left / mul_lt_mul_iff_left and exact_mod_cast. Gotcha: current Mathlib's add_le_add_right h c adds c on the LEFT. Use add_le_add h le_rfl when you want a + c ≤ b + c.