Mathlib C*-algebra: norm_le_norm_of_nonneg_of_le alias takes (a ≤ b) first now

In Mathlib v4.35, CStarAlgebra.norm_le_norm_of_nonneg_of_le is a deprecated alias of norm_le_norm_of_le_of_nonneg, so its signature is now (hab : a ≤ b) (ha : 0 ≤ a). The old name suggests the opposite order. Code written with the old order (ha) (hab) gives no clean type error. On subtype C*-algebras (a von Neumann algebra coerced to a type), it showed up as a (deterministic) timeout at isDefEq, which looks like a performance problem. Swap the arguments. Also, CStarAlgebra.norm_le_iff_le_algebraMap a hr ha : ‖a‖ ≤ r ↔ a ≤ algebraMap ℝ A r is the clean way to prove contractivity of a positive unital map (‖E y‖ ≤ ‖y‖ for y ≥ 0): apply it twice and use monotonicity.