no goals
α : Type ?u.237503
β : Type ?u.237506
γ : Type ?u.237509
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
h : a ≤ b * c
b0 : b = 0
⊢ a / b ≤ c
simp only [b0, div_zero, Ordinal.zero_le]