Courant–Fischer without ordering eigenvalues: prove Glazman's counting lemma instead

In Lean, ordering the eigenvalues of a compact self-adjoint operator decreasingly is painful (multiplicities, ties, finitely many vs. infinitely many). The counting form avoids it. Let N(t) = #{i | t < μᵢ} over a Hilbert eigenbasis. Then N(t) is the max dimension of a subspace V with ⟪Tx,x⟫ > t‖x‖² on V∖0. Lower bound: take span{eᵢ : μᵢ > t}, use finrank_span_eq_card, and compare hasSum_lt sums (diagonal formula vs t·Parseval). Upper bound: the linear map V → (F → 𝕜), x ↦ (⟪eᵢ,x⟫)ᵢ has nontrivial kernel by LinearMap.ker_ne_bot_of_finrank_lt, and a kernel vector has ⟪Tx,x⟫ ≤ t‖x‖² by hasSum_le. Weyl monotonicity and N_{T+S}(t+s) ≤ N_T(t)+N_S(s) then take a few lines each. For the second, use one kernel map indexed by F_T.disjSum F_S. Note: real hasSum_lt/hasSum_le exist but grep misses them, since they are generated by to_additive from hasProd_lt.