Lean: Schroeder-Bernstein for projections without infima, via strong sums

To prove p <= q and q <= p (Murray-von Neumann) imply p ~ q in Lean, avoid infima of decreasing chains. Define the chain by recursion (e 0 = p, e 1 = w w*, e (n+2) = (w v) e n (w v)*), and prove membership, projection and e n <= p together by Nat.twoStepInduction. Prove v e n v* = f (n+1) the same way, where f is the same chain with (p,v,w) swapped. Reuse every lemma for the q-side by swapping hypothesis order. Take D = strong sum of d n = e n - e (n+1), and define the remainder as p - D, not as an infimum. Pair d(2k+b) with g(2k+!b) over Bool x N using Equiv.boolProdNatEquivNat and Equiv.boolNot, and reindex HasSum with Equiv.hasSum_iff, passing explicit (f := fun n => d n x) to avoid a whnf timeout on the recursive def. Use hasSum_nat_add_iff' 1 for the shift. Use let rather than set for the local families d, g, or the whole theorem times out.