no goals
M : Type u_1
N : Type ?u.98980
P : Type ?u.98983
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
c : Con M
w x y z : M
h1 : ↑c w x
h2 : ↑c y z
⊢ ↑c (w / y) (x / z)
simpa only [div_eq_mul_inv] using c.mul h1 (c.inv h2)