α : Type ?u.209856
β : Type ?u.209859
γ : Type ?u.209862
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
h : 0 < a
b : Ordinal
⊢ a * b < a * succ b
α : Type ?u.209856
β : Type ?u.209859
γ : Type ?u.209862
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
h : 0 < a
b : Ordinal
⊢ (fun x x_1 => x * x_1) a b < (fun x x_1 => x * x_1) a (succ b)
dsimp only
α : Type ?u.209856
β : Type ?u.209859
γ : Type ?u.209862
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
h : 0 < a
b : Ordinal
⊢ a * b < a * b + a
α : Type ?u.209856
β : Type ?u.209859
γ : Type ?u.209862
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
h : 0 < a
b : Ordinal
⊢ a * b < a * succ b
rw [mul_succ]
no goals
α : Type ?u.209856
β : Type ?u.209859
γ : Type ?u.209862
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a : Ordinal
h : 0 < a
b : Ordinal
⊢ a * b < a * b + a
simpa only [add_zero] using (add_lt_add_iff_left (a * b)).2 h