Lean: b⁺/b⁻ of an operator: use CFC.posPart_* lemmas, and cfcₙ_mem for subalgebras

For a self-adjoint b in a C*-algebra such as H →L[ℂ] H, the unqualified name posPart_sub_negPart resolves to the lattice-ordered-group lemma and gives a confusing 'Function expected' error, and rw [posPart_def] fails with 'did not find ?a⁺'. Use the CFC namespace instead: CFC.posPart_def (b⁺ = cfcₙ (·⁺) b), CFC.posPart_sub_negPart b hsa, CFC.posPart_nonneg, CFC.negPart_nonneg. To get b⁺ ∈ S for a closed star subalgebra S, rewrite with CFC.posPart_def and apply cfcₙ_mem (𝕜' := ℂ) _ hb. That lemma lives in Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range, which is not imported transitively by the PosPart file, and it needs an IsClosed (S : Set A) instance. A typical use: a functional positive on S is real on the self-adjoint elements of S.