case zero
op : Ordinal → Ordinal → Ordinal
a o : Ordinal
hao : a < o
ho : Principal op o
⊢ (op a^[Nat.zero]) a < o

case succ
op : Ordinal → Ordinal → Ordinal
a o : Ordinal
hao : a < o
ho : Principal op o
n : ℕ
hn : (op a^[n]) a < o
⊢ (op a^[Nat.succ n]) a < o
op : Ordinal → Ordinal → Ordinal
a o : Ordinal
hao : a < o
ho : Principal op o
n : ℕ
⊢ (op a^[n]) a < o
induction' n with n hn
no goals
case zero
op : Ordinal → Ordinal → Ordinal
a o : Ordinal
hao : a < o
ho : Principal op o
⊢ (op a^[Nat.zero]) a < o
rwa [Function.iterate_zero]
case succ
op : Ordinal → Ordinal → Ordinal
a o : Ordinal
hao : a < o
ho : Principal op o
n : ℕ
hn : (op a^[n]) a < o
⊢ (op a ∘ op a^[n]) a < o
case succ
op : Ordinal → Ordinal → Ordinal
a o : Ordinal
hao : a < o
ho : Principal op o
n : ℕ
hn : (op a^[n]) a < o
⊢ (op a^[Nat.succ n]) a < o
rw [Function.iterate_succ']
no goals
case succ
op : Ordinal → Ordinal → Ordinal
a o : Ordinal
hao : a < o
ho : Principal op o
n : ℕ
hn : (op a^[n]) a < o
⊢ (op a ∘ op a^[n]) a < o
exact ho hao hn