b o✝ : Ordinal
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.snd
⊢ x ∈ CNF b o → 0 < x.snd
b o : Ordinal
x : Ordinal × Ordinal
⊢ x ∈ CNF b o → 0 < x.snd
refine' CNFRec b (by simp) (fun o ho IH ↦ _) o
b o✝ : Ordinal
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.snd
⊢ x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → 0 < x.snd
b o✝ : Ordinal
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.snd
⊢ x ∈ CNF b o → 0 < x.snd
rw [CNF_ne_zero ho]
case head
b o✝ o : Ordinal
ho : o ≠ 0
IH : (log b o, o / b ^ log b o) ∈ CNF b (o % b ^ log b o) → 0 < (log b o, o / b ^ log b o).snd
⊢ 0 < (log b o, o / b ^ log b o).snd

case tail
b o✝ : Ordinal
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.snd
h : Mem x (CNF b (o % b ^ log b o))
⊢ 0 < x.snd
b o✝ : Ordinal
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.snd
⊢ x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → 0 < x.snd
rintro (h | ⟨_, h⟩)
no goals
b o : Ordinal
x : Ordinal × Ordinal
⊢ x ∈ CNF b 0 → 0 < x.snd
simp
no goals
case head
b o✝ o : Ordinal
ho : o ≠ 0
IH : (log b o, o / b ^ log b o) ∈ CNF b (o % b ^ log b o) → 0 < (log b o, o / b ^ log b o).snd
⊢ 0 < (log b o, o / b ^ log b o).snd
exact div_opow_log_pos b ho
no goals
case tail
b o✝ : Ordinal
x : Ordinal × Ordinal
o : Ordinal
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.snd
h : Mem x (CNF b (o % b ^ log b o))
⊢ 0 < x.snd
exact IH h