no goals
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
x : R
⊢ 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
simp only [le_iff, zero_add, exists_eq_right']