have h' := mult_right G (G.inv a) (b * a) (c * a) h
α : Type u_1
G : group α
a b c : α
h : b * a = c * a
⊢ b = c
α : Type u_1
G : group α
a b c : α
h : b * a = c * a
h' : b * a * group.inv a = c * a * group.inv a
⊢ b = c