Product of commuting nonnegative elements is nonnnegative

theorem CFC.sqrt_eq_cfcₙ_real_sqrt {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [TopologicalSpace A] [T2Space A] [IsTopologicalRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] (a : A) (ha : 0 ≤ a := by cfc_tac) : sqrt a = cfcₙ Real.sqrt a

theorem Commute.mul_nonneg {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a b : A} (hab : Commute a b) (ha : 0 ≤ a := by cfc_tac) (hb : 0 ≤ b := by cfc_tac) : 0 ≤ a * b

theorem CStarAlgebra.prod_nonneg_of_commute {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {l : List A} (hl_nonneg : ∀ x ∈ l, 0 ≤ x) (hl_comm : ∀ x ∈ l, ∀ y ∈ l, Commute x y) : 0 ≤ l.prod