op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
ha : ∃ n, a < (blsub₂ op^[n]) o
hb : ∃ n, b < (blsub₂ op^[n]) o
⊢ ∃ n, op a b < (blsub₂ op^[n]) o
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
ha : a < nfp (blsub₂ op) o
hb : b < nfp (blsub₂ op) o
⊢ op a b < nfp (blsub₂ op) o
rw [lt_nfp] at *
case intro
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
hb : ∃ n, b < (blsub₂ op^[n]) o
m : ℕ
hm : a < (blsub₂ op^[m]) o
⊢ ∃ n, op a b < (blsub₂ op^[n]) o
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
ha : ∃ n, a < (blsub₂ op^[n]) o
hb : ∃ n, b < (blsub₂ op^[n]) o
⊢ ∃ n, op a b < (blsub₂ op^[n]) o
cases' ha with m hm
case intro.intro
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
m : ℕ
hm : a < (blsub₂ op^[m]) o
n : ℕ
hn : b < (blsub₂ op^[n]) o
⊢ ∃ n, op a b < (blsub₂ op^[n]) o
case intro
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
hb : ∃ n, b < (blsub₂ op^[n]) o
m : ℕ
hm : a < (blsub₂ op^[m]) o
⊢ ∃ n, op a b < (blsub₂ op^[n]) o
cases' hb with n hn
case intro.intro.inl
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
m : ℕ
hm : a < (blsub₂ op^[m]) o
n : ℕ
hn : b < (blsub₂ op^[n]) o
h : (blsub₂ op^[m]) o ≤ (blsub₂ op^[n]) o
⊢ ∃ n, op a b < (blsub₂ op^[n]) o

case intro.intro.inr
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
m : ℕ
hm : a < (blsub₂ op^[m]) o
n : ℕ
hn : b < (blsub₂ op^[n]) o
h : (blsub₂ op^[n]) o ≤ (blsub₂ op^[m]) o
⊢ ∃ n, op a b < (blsub₂ op^[n]) o
case intro.intro
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
m : ℕ
hm : a < (blsub₂ op^[m]) o
n : ℕ
hn : b < (blsub₂ op^[n]) o
⊢ ∃ n, op a b < (blsub₂ op^[n]) o
cases' le_total ((blsub₂.{u, u} op^[m]) o) ((blsub₂.{u, u} op^[n]) o) with h h
case intro.intro.inl
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
m : ℕ
hm : a < (blsub₂ op^[m]) o
n : ℕ
hn : b < (blsub₂ op^[n]) o
h : (blsub₂ op^[m]) o ≤ (blsub₂ op^[n]) o
⊢ op a b < (blsub₂ op^[n + 1]) o
case intro.intro.inl
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
m : ℕ
hm : a < (blsub₂ op^[m]) o
n : ℕ
hn : b < (blsub₂ op^[n]) o
h : (blsub₂ op^[m]) o ≤ (blsub₂ op^[n]) o
⊢ ∃ n, op a b < (blsub₂ op^[n]) o
use n + 1
case intro.intro.inl
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
m : ℕ
hm : a < (blsub₂ op^[m]) o
n : ℕ
hn : b < (blsub₂ op^[n]) o
h : (blsub₂ op^[m]) o ≤ (blsub₂ op^[n]) o
⊢ op a b < (blsub₂ op ∘ blsub₂ op^[n]) o
case intro.intro.inl
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
m : ℕ
hm : a < (blsub₂ op^[m]) o
n : ℕ
hn : b < (blsub₂ op^[n]) o
h : (blsub₂ op^[m]) o ≤ (blsub₂ op^[n]) o
⊢ op a b < (blsub₂ op^[n + 1]) o
rw [Function.iterate_succ']
no goals
case intro.intro.inl
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
m : ℕ
hm : a < (blsub₂ op^[m]) o
n : ℕ
hn : b < (blsub₂ op^[n]) o
h : (blsub₂ op^[m]) o ≤ (blsub₂ op^[n]) o
⊢ op a b < (blsub₂ op ∘ blsub₂ op^[n]) o
exact lt_blsub₂ op (hm.trans_le h) hn
case intro.intro.inr
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
m : ℕ
hm : a < (blsub₂ op^[m]) o
n : ℕ
hn : b < (blsub₂ op^[n]) o
h : (blsub₂ op^[n]) o ≤ (blsub₂ op^[m]) o
⊢ op a b < (blsub₂ op^[m + 1]) o
case intro.intro.inr
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
m : ℕ
hm : a < (blsub₂ op^[m]) o
n : ℕ
hn : b < (blsub₂ op^[n]) o
h : (blsub₂ op^[n]) o ≤ (blsub₂ op^[m]) o
⊢ ∃ n, op a b < (blsub₂ op^[n]) o
use m + 1
case intro.intro.inr
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
m : ℕ
hm : a < (blsub₂ op^[m]) o
n : ℕ
hn : b < (blsub₂ op^[n]) o
h : (blsub₂ op^[n]) o ≤ (blsub₂ op^[m]) o
⊢ op a b < (blsub₂ op ∘ blsub₂ op^[m]) o
case intro.intro.inr
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
m : ℕ
hm : a < (blsub₂ op^[m]) o
n : ℕ
hn : b < (blsub₂ op^[n]) o
h : (blsub₂ op^[n]) o ≤ (blsub₂ op^[m]) o
⊢ op a b < (blsub₂ op^[m + 1]) o
rw [Function.iterate_succ']
no goals
case intro.intro.inr
op : Ordinal → Ordinal → Ordinal
o a b : Ordinal
m : ℕ
hm : a < (blsub₂ op^[m]) o
n : ℕ
hn : b < (blsub₂ op^[n]) o
h : (blsub₂ op^[n]) o ≤ (blsub₂ op^[m]) o
⊢ op a b < (blsub₂ op ∘ blsub₂ op^[m]) o
exact lt_blsub₂ op hm (hn.trans_le h)