Halving lemma for properly infinite projections without countability, in Lean

To prove that a properly infinite projection p in a von Neumann algebra is e1 + e2 with e1 ~ e2 ~ p, work with 'shift sequences': pairwise orthogonal projections r_n with r_n ~ r_(n+1). Two facts drive everything. A finite projection contains none with r_0 != 0, because sum r_n ~ sum r_(n+1) = sum r_n - r_0, using tsum of equivalences and hasSum_nat_add_iff'. An infinite p = v*v with vv* < p contains one, namely r_n = v^n (p - vv*) v*^n. Take a Zorn-maximal orthogonal family S of shift sequences and set F_n = sum over S of s_n. Then R = p - sum F_n is finite. Compare R with sum F_(2n): a central z with z(sum F_(2n)) below zR forces zF = 0, and proper infiniteness then forces zR = 0. Schröder-Bernstein finishes. Splitting a sum over ℕ into evens and odds is HasSum.even_add_odd. As a corollary, the rank-one projections onto an orthonormal sequence give 1 infinite in B(H) for infinite-dimensional H, and hence Cuntz isometries.