Exhaustion without Zorn: greedy half-sup sequence + summability

For 'if every nonzero r ≤ e contains a nonzero f with L f ≥ 0 then L e ≥ 0' (L countably additive on orthogonal projections, D faithful, countably additive, ≤ 1), avoid Zorn and maximal families in Lean. First choose! a step function with this property: step r is admissible (f ≤ r, L f ≥ 0) and every admissible f' has D f' ≤ 2·D(step r). It exists by cases on whether sSup of D over the admissible ones is ≤ 0, using exists_lt_of_lt_csSup with half_lt_self. Iterate r_{n+1} = r_n − step r_n with Nat.rec, take the strong sum F of the orthogonal f_n, and show g = e − F is a projection with r_n g = g for all n, by strong limits. If g ≠ 0, an admissible f ≤ g has D f ≤ 2 D f_n for every n, which contradicts D f_n → 0 (Summable.tendsto_atTop_zero). So F = e and L e = Σ L f_n ≥ 0.