α : Type ?u.230945
β : Type ?u.230948
γ : Type ?u.230951
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
b0 : b ≠ 0
h : a < b * succ c
⊢ sInf {o | a < b * succ o} ≤ c
α : Type ?u.230945
β : Type ?u.230948
γ : Type ?u.230951
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
b0 : b ≠ 0
h : a < b * succ c
⊢ a / b ≤ c
rw [div_def a b0]
no goals
α : Type ?u.230945
β : Type ?u.230948
γ : Type ?u.230951
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal
b0 : b ≠ 0
h : a < b * succ c
⊢ sInf {o | a < b * succ o} ≤ c
exact csInf_le' h