case h
a✝ b c a : Ordinal
IH : ∀ (k : Ordinal), k < a → k ♯ 1 = succ k
⊢ a ♯ 1 = succ a
a b c : Ordinal
⊢ a ♯ 1 = succ a
induction' a using Ordinal.induction with a IH
case h
a✝ b c a : Ordinal
IH : ∀ (k : Ordinal), k < a → k ♯ 1 = succ k
⊢ ∀ (i : Ordinal), i < a → i ♯ 1 < succ a
case h
a✝ b c a : Ordinal
IH : ∀ (k : Ordinal), k < a → k ♯ 1 = succ k
⊢ a ♯ 1 = succ a
rw [nadd_def, blsub_one, nadd_zero, max_eq_right_iff, blsub_le_iff]
case h
a✝ b c a : Ordinal
IH : ∀ (k : Ordinal), k < a → k ♯ 1 = succ k
i : Ordinal
hi : i < a
⊢ i ♯ 1 < succ a
case h
a✝ b c a : Ordinal
IH : ∀ (k : Ordinal), k < a → k ♯ 1 = succ k
⊢ ∀ (i : Ordinal), i < a → i ♯ 1 < succ a
intro i hi
no goals
case h
a✝ b c a : Ordinal
IH : ∀ (k : Ordinal), k < a → k ♯ 1 = succ k
i : Ordinal
hi : i < a
⊢ i ♯ 1 < succ a
rwa [IH i hi, succ_lt_succ_iff]