have rel_xy := self_inv_of_squares_id h (y * x)
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
⊢ x * y = y * x
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
rel_xy : (y * x)⁻¹ = y * x
⊢ x * y = y * x