no goals
R : Type u
inst✝² : NonUnitalSemiring R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
a b : R
hab : a ≤ b
c : R
⊢ c * a * star c ≤ c * b * star c
simpa only [star_star] using conjugate_le_conjugate hab (star c)