no goals
α : Type ?u.243802
β : Type ?u.243805
γ : Type ?u.243808
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
b0 : b ≠ 0
⊢ b * a / b = a
simpa only [add_zero, zero_div] using mul_add_div a b0 0