no goals
M : Type u_1
N : Type ?u.96860
P : Type ?u.96863
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
c : Con M
x y : M
h : ↑c x y
⊢ ↑c x⁻¹ y⁻¹
simpa using c.symm (c.mul (c.mul (c.refl x⁻¹) h) (c.refl y⁻¹))