no goals
α : Type ?u.133611
β : Type ?u.133614
γ : Type ?u.133617
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
l : IsLimit a
h : b < a
⊢ b + 0 < a
rwa [add_zero]
α : Type ?u.133611
β : Type ?u.133614
γ : Type ?u.133617
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
l : IsLimit a
h✝ : b < a
c : Ordinal
h : c < a - b
⊢ succ (b + c) < a
α : Type ?u.133611
β : Type ?u.133614
γ : Type ?u.133617
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
l : IsLimit a
h✝ : b < a
c : Ordinal
h : c < a - b
⊢ succ c < a - b
rw [lt_sub, add_succ]
no goals
α : Type ?u.133611
β : Type ?u.133614
γ : Type ?u.133617
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
l : IsLimit a
h✝ : b < a
c : Ordinal
h : c < a - b
⊢ succ (b + c) < a
exact l.2 _ (lt_sub.1 h)