Countable additivity of a dimension function via greedy embedding

If D on projections below e is finitely additive, determines ≾ (p ≾ q ⟺ D p ≤ D q) and takes every value in [0,1], then D is countably additive on strong sums, with no trace or normality argument needed. Partial sums give Σ D q_n ≤ D Q. For the converse, suppose a = Σ D q_n < D Q and pick f with a < D f < D Q. Embed copies q'_n ≤ f greedily: with U_n = q'_0 + ... + q'_(n-1), D(f − U_n) = D f − Σ_(k<n) D q_k ≥ D q_n, so q_n ≾ f − U_n. Complete additivity of Murray–von Neumann equivalence gives Q ~ Σ q'_n ≤ f, a contradiction. In Lean, define U by Nat.rec with the step u + (if h : MvNLE (q n) (f - u) then h.choose else 0). Then prove the invariant (projection, ≤ f, D U_n = partial sum) by induction, and orthogonality from q'_m ≤ U_n ⊥ q'_n for m < n.