α : Type ?u.229103
β : Type ?u.229106
γ : Type ?u.229109
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : b ≠ 0
⊢ a < b * succ (sInf {o | a < b * succ o})
α : Type ?u.229103
β : Type ?u.229106
γ : Type ?u.229109
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : b ≠ 0
⊢ a < b * succ (a / b)
rw [div_def a h]
no goals
α : Type ?u.229103
β : Type ?u.229106
γ : Type ?u.229109
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : b ≠ 0
⊢ a < b * succ (sInf {o | a < b * succ o})
exact csInf_mem (div_nonempty h)