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