case inl
α : Type ?u.99924
r : α → α → Prop
a : Ordinal
h : 0 ≠ 0
⊢ cof (a + 0) = cof 0

case inr.inl.intro
α : Type ?u.99924
r : α → α → Prop
a c : Ordinal
h : succ c ≠ 0
⊢ cof (a + succ c) = cof (succ c)

case inr.inr
α : Type ?u.99924
r : α → α → Prop
a b : Ordinal
h : b ≠ 0
hb : IsLimit b
⊢ cof (a + b) = cof b
α : Type ?u.99924
r : α → α → Prop
a b : Ordinal
h : b ≠ 0
⊢ cof (a + b) = cof b
rcases zero_or_succ_or_limit b with (rfl | ⟨c, rfl⟩ | hb)
no goals
case inl
α : Type ?u.99924
r : α → α → Prop
a : Ordinal
h : 0 ≠ 0
⊢ cof (a + 0) = cof 0
contradiction
no goals
case inr.inl.intro
α : Type ?u.99924
r : α → α → Prop
a c : Ordinal
h : succ c ≠ 0
⊢ cof (a + succ c) = cof (succ c)
rw [add_succ, cof_succ, cof_succ]
no goals
case inr.inr
α : Type ?u.99924
r : α → α → Prop
a b : Ordinal
h : b ≠ 0
hb : IsLimit b
⊢ cof (a + b) = cof b
exact (add_isNormal a).cof_eq hb