α : Type ?u.243145
β : Type ?u.243148
γ : Type ?u.243151
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : a < b
⊢ a < b * succ 0
α : Type ?u.243145
β : Type ?u.243148
γ : Type ?u.243151
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : a < b
⊢ a / b = 0
rw [← Ordinal.le_zero, div_le <| Ordinal.pos_iff_ne_zero.1 <| (Ordinal.zero_le _).trans_lt h]
no goals
α : Type ?u.243145
β : Type ?u.243148
γ : Type ?u.243151
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : a < b
⊢ a < b * succ 0
simpa only [succ_zero, mul_one] using h