no goals
α : Type ?u.251122
β : Type ?u.251125
γ : Type ?u.251128
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
a0 : a ≠ 0
b : Ordinal
⊢ a * (a * b / a) = a * b
rw [mul_div_cancel _ a0]