no goals
α : Type ?u.244913
β : Type ?u.244916
γ : Type ?u.244919
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
⊢ a / 1 = a
simpa only [one_mul] using mul_div_cancel a Ordinal.one_ne_zero