Theorem: Subsemigroup.prodProperty_iff_of_comm (Kaplanski4/Absorbing.lean)

State before:
M : Type u_1
N : Type ?u.11134
inst✝ : CommMonoid M
S : Subsemigroup M
h : ∀ (x y : M), x * y ∈ S → ∃ z ∈ S, Associated x z
x y : M
hxy : x * y ∈ S
⊢ y * x ∈ S
Tactic:
rwa [mul_comm] at hxy
State after:
no goals