case inl
α : Type ?u.129526
β : Type ?u.129529
γ : Type ?u.129532
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : b ≤ a
e : a - b = 0
⊢ b + (a - b) ≤ a

case inr.inl.intro
α : Type ?u.129526
β : Type ?u.129529
γ : Type ?u.129532
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : b ≤ a
c : Ordinal
e : a - b = succ c
⊢ b + (a - b) ≤ a

case inr.inr
α : Type ?u.129526
β : Type ?u.129529
γ : Type ?u.129532
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : b ≤ a
l : IsLimit (a - b)
⊢ b + (a - b) ≤ a
α : Type ?u.129526
β : Type ?u.129529
γ : Type ?u.129532
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : b ≤ a
⊢ b + (a - b) ≤ a
rcases zero_or_succ_or_limit (a - b) with (e | ⟨c, e⟩ | l)
no goals
case inl
α : Type ?u.129526
β : Type ?u.129529
γ : Type ?u.129532
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : b ≤ a
e : a - b = 0
⊢ b + (a - b) ≤ a
simp only [e, add_zero, h]
case inr.inl.intro
α : Type ?u.129526
β : Type ?u.129529
γ : Type ?u.129532
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : b ≤ a
c : Ordinal
e : a - b = succ c
⊢ c < succ c
case inr.inl.intro
α : Type ?u.129526
β : Type ?u.129529
γ : Type ?u.129532
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : b ≤ a
c : Ordinal
e : a - b = succ c
⊢ b + (a - b) ≤ a
rw [e, add_succ, succ_le_iff, ← lt_sub, e]
no goals
case inr.inl.intro
α : Type ?u.129526
β : Type ?u.129529
γ : Type ?u.129532
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : b ≤ a
c : Ordinal
e : a - b = succ c
⊢ c < succ c
exact lt_succ c
no goals
case inr.inr
α : Type ?u.129526
β : Type ?u.129529
γ : Type ?u.129532
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal
h : b ≤ a
l : IsLimit (a - b)
⊢ b + (a - b) ≤ a
exact (add_le_of_limit l).2 fun c l => (lt_sub.1 l).le