From c1ff2300079ce25d0302835b9fee3caf0964ad3f Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Thu, 12 Mar 2026 23:50:05 -0600
Subject: [PATCH 1/9] start

---
 CombinatorialGames/NatOrdinal/Pow.lean | 39 ++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

diff --git a/CombinatorialGames/NatOrdinal/Pow.lean b/CombinatorialGames/NatOrdinal/Pow.lean
index 65b93772..82a34126 100644
--- a/CombinatorialGames/NatOrdinal/Pow.lean
+++ b/CombinatorialGames/NatOrdinal/Pow.lean
@@ -8,6 +8,8 @@ module
 public import CombinatorialGames.NatOrdinal.Basic
 public import Mathlib.SetTheory.Ordinal.Exponential
 
+import CombinatorialGames.Tactic.OrdinalAlias
+
 /-!
 # Natural operations on `ω ^ x`
 
@@ -37,6 +39,22 @@ theorem Ordinal.lt_mul_add_one {x y z : Ordinal} : x < y * (z + 1) ↔ ∃ w < y
   · simp
   · rw [mul_add_one, lt_add_iff hy]
 
+theorem Ordinal.opow_mul_lt_opow {b u v x : Ordinal} (hv : v < b) (hu : u < x) :
+    b ^ u * v < b ^ x := by
+  simpa using Ordinal.opow_mul_add_lt_opow hv (opow_pos _ hv.pos) hu
+
+theorem Ordinal.lt_omega0_omega0_opow {x y : Ordinal} (hy : y ≠ 0) :
+    x < ω ^ ω ^ y ↔ ∃ z < y, ∃ n : ℕ, x < ω ^ (ω ^ z * n) := by
+  simp_rw [lt_omega0_opow (opow_ne_zero _ omega0_ne_zero), lt_omega0_opow hy]
+  constructor
+  · intro ⟨a, ⟨b, hb, ⟨m, hm⟩⟩, ⟨n, hn⟩⟩
+    exact ⟨_, hb, _, hn.trans <| opow_mul_lt_opow (natCast_lt_omega0 _) <|
+      hm.trans_le (mul_le_mul_right (Nat.cast_le.2 m.le_succ) _)⟩
+  · intro ⟨a, ha, ⟨n, hn⟩⟩
+    refine ⟨ω ^ a * n, ⟨a, ha, n + 1, ?_⟩, 1, ?_⟩
+    · simp [mul_lt_mul_iff_right₀, opow_pos]
+    · simpa
+
 /-- A typeclass for the the `ω^` notation. -/
 class Wpow (α : Type*) where
   /-- The `ω`-map, i.e. base `ω` exponentiation. -/
@@ -58,6 +76,7 @@ theorem wpow_def (x : NatOrdinal) : ω^ x = of (ω ^ x.val) := rfl
 @[simp] theorem wpow_zero : ω^ (0 : NatOrdinal) = 1 := by simp [wpow_def]
 @[simp] theorem wpow_pos (x : NatOrdinal) : 0 < ω^ x := opow_pos _ omega0_pos
 @[simp] theorem wpow_ne_zero (x : NatOrdinal) : ω^ x ≠ 0 := (wpow_pos x).ne'
+@[simp] theorem wpow_one : ω^ (1 : NatOrdinal) = of ω := by simp [wpow_def]
 
 theorem isNormal_wpow : Order.IsNormal (ω^ · : NatOrdinal → NatOrdinal) :=
   Ordinal.isNormal_opow one_lt_omega0
@@ -135,6 +154,10 @@ theorem wpow_mul_natCast_lt (h : x < y) (n : ℕ) : ω^ x * n < ω^ y := by
   rw [wpow_mul_natCast]
   exact omega0_opow_mul_nat_lt h n
 
+@[simp]
+theorem of_opow_mul_natCast (x : Ordinal) (n : ℕ) : of (ω ^ x * n) = ω^ of x * n := by
+  simpa using (wpow_mul_natCast (of x) n).symm
+
 theorem lt_wpow_iff (hx : x ≠ 0) : y < ω^ x ↔ ∃ z < x, ∃ n : ℕ, y < ω^ z * n := by
   rw [wpow_def, ← val_lt_iff, lt_omega0_opow]
   · simp_rw [wpow_mul_natCast]
@@ -196,5 +219,21 @@ theorem wpow_add (x y : NatOrdinal) : ω^ (x + y) = ω^ x * ω^ y := by
       exact wpow_mul_natCast_lt (add_lt_add_right hb x) m
 termination_by (x, y)
 
+theorem mul_lt_wpow_wpow (hx : x < ω^ ω^ z) (hy : y < ω^ ω^ z) : x * y < ω^ ω^ z := by
+  induction x with | mk x
+  induction y with | mk y
+  obtain rfl | hz := eq_or_ne z 0
+  · simp_rw [wpow_zero, wpow_one, of.lt_iff_lt, Ordinal.lt_omega0] at hx hy
+    obtain ⟨m, rfl⟩ := hx
+    obtain ⟨n, rfl⟩ := hy
+    simpa [← Nat.cast_mul] using Ordinal.natCast_lt_omega0 (m * n)
+  · rw [← val_ne_zero] at hz
+    rw [wpow_def, of.lt_iff_lt, val_wpow, lt_omega0_omega0_opow hz] at hx hy
+    obtain ⟨a, ha, m, hm⟩ := hx
+    obtain ⟨b, hb, n, hn⟩ := hy
+    rw [← of.lt_iff_lt] at hm hn
+    apply (mul_le_mul' hm.le hn.le).trans_lt
+    simpa [← wpow_add] using add_lt_wpow (wpow_mul_natCast_lt ha m) (wpow_mul_natCast_lt hb n)
+
 end NatOrdinal
 end

From 693df6022478e3d12442360f42a2b2b930d1d0b3 Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Thu, 12 Mar 2026 23:51:22 -0600
Subject: [PATCH 2/9] prove theorem

---
 CombinatorialGames/NatOrdinal/Basic.lean    | 14 ++++++++++++++
 CombinatorialGames/Tactic/OrdinalAlias.lean |  2 ++
 2 files changed, 16 insertions(+)

diff --git a/CombinatorialGames/NatOrdinal/Basic.lean b/CombinatorialGames/NatOrdinal/Basic.lean
index a75cfdb9..53b5c94a 100644
--- a/CombinatorialGames/NatOrdinal/Basic.lean
+++ b/CombinatorialGames/NatOrdinal/Basic.lean
@@ -172,6 +172,20 @@ instance : AddMonoidWithOne NatOrdinal where
 @[simp] theorem of_natCast (n : ℕ) : of n = n := rfl
 @[simp] theorem val_natCast (n : ℕ) : val n = n := rfl
 
+@[simp, norm_cast] theorem natCast_le_of_iff {a : ℕ} {b : Ordinal} : a ≤ of b ↔ a ≤ b := .rfl
+@[simp, norm_cast] theorem natCast_lt_of_iff {a : ℕ} {b : Ordinal} : a < of b ↔ a < b := .rfl
+@[simp, norm_cast] theorem natCast_eq_of_iff {a : ℕ} {b : Ordinal} : a = of b ↔ a = b := .rfl
+@[simp, norm_cast] theorem natCast_le_val_iff {a : ℕ} {b : NatOrdinal} : a ≤ val b ↔ a ≤ b := .rfl
+@[simp, norm_cast] theorem natCast_lt_val_iff {a : ℕ} {b : NatOrdinal} : a < val b ↔ a < b := .rfl
+@[simp, norm_cast] theorem natCast_eq_val_iff {a : ℕ} {b : NatOrdinal} : a = val b ↔ a = b := .rfl
+
+@[simp, norm_cast] theorem of_le_natCast_iff {a : Ordinal} {b : ℕ} : of a ≤ b ↔ a ≤ b := .rfl
+@[simp, norm_cast] theorem of_lt_natCast_iff {a : Ordinal} {b : ℕ} : of a < b ↔ a < b := .rfl
+@[simp, norm_cast] theorem of_eq_natCast_iff {a : Ordinal} {b : ℕ} : of a = b ↔ a = b := .rfl
+@[simp, norm_cast] theorem val_le_natCast_iff {a : NatOrdinal} {b : ℕ} : val a ≤ b ↔ a ≤ b := .rfl
+@[simp, norm_cast] theorem val_lt_natCast_iff {a : NatOrdinal} {b : ℕ} : val a < b ↔ a < b := .rfl
+@[simp, norm_cast] theorem val_eq_natCast_iff {a : NatOrdinal} {b : ℕ} : val a = b ↔ a = b := .rfl
+
 @[simp] protected theorem succ_one : succ (1 : NatOrdinal) = 2 := Ordinal.succ_one
 
 @[simp]
diff --git a/CombinatorialGames/Tactic/OrdinalAlias.lean b/CombinatorialGames/Tactic/OrdinalAlias.lean
index ee942be9..e9035c7f 100644
--- a/CombinatorialGames/Tactic/OrdinalAlias.lean
+++ b/CombinatorialGames/Tactic/OrdinalAlias.lean
@@ -120,6 +120,8 @@ theorem $(mkIdent `val_image_Iio) (a) : $(mkVal Alias) '' Set.Iio a = Set.Iio ($
 
 @[simp] theorem $(mkIdent `of_eq_zero) {a} : $(mkOf Alias) a = 0 ↔ a = 0 := .rfl
 @[simp] theorem $(mkIdent `val_eq_zero) {a} : $(mkVal Alias) a = 0 ↔ a = 0 := .rfl
+@[simp] theorem $(mkIdent `of_ne_zero) {a} : $(mkOf Alias) a ≠ 0 ↔ a ≠ 0 := .rfl
+@[simp] theorem $(mkIdent `val_ne_zero) {a} : $(mkVal Alias) a ≠ 0 ↔ a ≠ 0 := .rfl
 
 @[simp] theorem $(mkIdent `of_eq_one) {a} : $(mkOf Alias) a = 1 ↔ a = 1 := .rfl
 @[simp] theorem $(mkIdent `val_eq_one) {a} : $(mkVal Alias) a = 1 ↔ a = 1 := .rfl

From 8f512c5eb8ba7d1f885ad90afdaa836ce02bd4ea Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Thu, 12 Mar 2026 23:51:51 -0600
Subject: [PATCH 3/9] don't need

---
 CombinatorialGames/NatOrdinal/Pow.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/CombinatorialGames/NatOrdinal/Pow.lean b/CombinatorialGames/NatOrdinal/Pow.lean
index 82a34126..4b58cb3e 100644
--- a/CombinatorialGames/NatOrdinal/Pow.lean
+++ b/CombinatorialGames/NatOrdinal/Pow.lean
@@ -8,8 +8,6 @@ module
 public import CombinatorialGames.NatOrdinal.Basic
 public import Mathlib.SetTheory.Ordinal.Exponential
 
-import CombinatorialGames.Tactic.OrdinalAlias
-
 /-!
 # Natural operations on `ω ^ x`
 

From 096cbe57f5bc5cc19b1e8027da3878cf2812672c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez=20Palacios?= <vi.hdz.p@gmail.com>
Date: Fri, 13 Mar 2026 00:41:21 -0600
Subject: [PATCH 4/9] simp is redundant

---
 CombinatorialGames/Tactic/OrdinalAlias.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CombinatorialGames/Tactic/OrdinalAlias.lean b/CombinatorialGames/Tactic/OrdinalAlias.lean
index e9035c7f..3f67907b 100644
--- a/CombinatorialGames/Tactic/OrdinalAlias.lean
+++ b/CombinatorialGames/Tactic/OrdinalAlias.lean
@@ -120,8 +120,8 @@ theorem $(mkIdent `val_image_Iio) (a) : $(mkVal Alias) '' Set.Iio a = Set.Iio ($
 
 @[simp] theorem $(mkIdent `of_eq_zero) {a} : $(mkOf Alias) a = 0 ↔ a = 0 := .rfl
 @[simp] theorem $(mkIdent `val_eq_zero) {a} : $(mkVal Alias) a = 0 ↔ a = 0 := .rfl
-@[simp] theorem $(mkIdent `of_ne_zero) {a} : $(mkOf Alias) a ≠ 0 ↔ a ≠ 0 := .rfl
-@[simp] theorem $(mkIdent `val_ne_zero) {a} : $(mkVal Alias) a ≠ 0 ↔ a ≠ 0 := .rfl
+theorem $(mkIdent `of_ne_zero) {a} : $(mkOf Alias) a ≠ 0 ↔ a ≠ 0 := .rfl
+theorem $(mkIdent `val_ne_zero) {a} : $(mkVal Alias) a ≠ 0 ↔ a ≠ 0 := .rfl
 
 @[simp] theorem $(mkIdent `of_eq_one) {a} : $(mkOf Alias) a = 1 ↔ a = 1 := .rfl
 @[simp] theorem $(mkIdent `val_eq_one) {a} : $(mkVal Alias) a = 1 ↔ a = 1 := .rfl

From 82ca5d73d8ad2a738a16cf213130f58f624edb0d Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Fri, 13 Mar 2026 15:31:07 -0600
Subject: [PATCH 5/9] merge

---
 CombinatorialGames/NatOrdinal/Pow.lean | 21 +++------------------
 1 file changed, 3 insertions(+), 18 deletions(-)

diff --git a/CombinatorialGames/NatOrdinal/Pow.lean b/CombinatorialGames/NatOrdinal/Pow.lean
index 4b58cb3e..ccb4ca5f 100644
--- a/CombinatorialGames/NatOrdinal/Pow.lean
+++ b/CombinatorialGames/NatOrdinal/Pow.lean
@@ -32,27 +32,12 @@ notation `ω^ x` for `of (ω ^ x.val)`. This typeclass will get reused for `IGam
 
 open Ordinal
 
-theorem Ordinal.lt_mul_add_one {x y z : Ordinal} : x < y * (z + 1) ↔ ∃ w < y, x ≤ y * z + w := by
+theorem Ordinal.lt_mul_add_one_iff {x y z : Ordinal} :
+    x < y * (z + 1) ↔ ∃ w < y, x ≤ y * z + w := by
   obtain rfl | hy := eq_or_ne y 0
   · simp
   · rw [mul_add_one, lt_add_iff hy]
 
-theorem Ordinal.opow_mul_lt_opow {b u v x : Ordinal} (hv : v < b) (hu : u < x) :
-    b ^ u * v < b ^ x := by
-  simpa using Ordinal.opow_mul_add_lt_opow hv (opow_pos _ hv.pos) hu
-
-theorem Ordinal.lt_omega0_omega0_opow {x y : Ordinal} (hy : y ≠ 0) :
-    x < ω ^ ω ^ y ↔ ∃ z < y, ∃ n : ℕ, x < ω ^ (ω ^ z * n) := by
-  simp_rw [lt_omega0_opow (opow_ne_zero _ omega0_ne_zero), lt_omega0_opow hy]
-  constructor
-  · intro ⟨a, ⟨b, hb, ⟨m, hm⟩⟩, ⟨n, hn⟩⟩
-    exact ⟨_, hb, _, hn.trans <| opow_mul_lt_opow (natCast_lt_omega0 _) <|
-      hm.trans_le (mul_le_mul_right (Nat.cast_le.2 m.le_succ) _)⟩
-  · intro ⟨a, ha, ⟨n, hn⟩⟩
-    refine ⟨ω ^ a * n, ⟨a, ha, n + 1, ?_⟩, 1, ?_⟩
-    · simp [mul_lt_mul_iff_right₀, opow_pos]
-    · simpa
-
 /-- A typeclass for the the `ω^` notation. -/
 class Wpow (α : Type*) where
   /-- The `ω`-map, i.e. base `ω` exponentiation. -/
@@ -116,7 +101,7 @@ private theorem wpow_mul_natCast_add_of_lt_aux {x y : NatOrdinal} (hy : y < ω^
           obtain (⟨a, ha, hz⟩ | h) := lt_add_iff.1 hz
           · have hxn := (wpow_mul_natCast_add_of_lt_aux (wpow_pos x) (n + 1)).2
             simp_rw [val_zero, add_zero] at hxn
-            rw [hxn, ← val_lt_iff, Nat.cast_add_one, lt_mul_add_one] at ha
+            rw [hxn, ← val_lt_iff, Nat.cast_add_one, lt_mul_add_one_iff] at ha
             obtain ⟨b, (hb : of b < ω^ x), hbw⟩ := ha
             rw [val_le_iff, ← val_of b, ← (wpow_mul_natCast_add_of_lt_aux hb n).2] at hbw
             refine ⟨_, hb, hz.trans <| (add_le_add_left hbw _).trans ?_⟩

From 5110b9acd3c97da8e9ae706a273899ad7f54dba5 Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Mon, 16 Mar 2026 01:40:56 -0600
Subject: [PATCH 6/9] refix

---
 CombinatorialGames/NatOrdinal/Pow.lean | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/CombinatorialGames/NatOrdinal/Pow.lean b/CombinatorialGames/NatOrdinal/Pow.lean
index ccb4ca5f..8d07bc88 100644
--- a/CombinatorialGames/NatOrdinal/Pow.lean
+++ b/CombinatorialGames/NatOrdinal/Pow.lean
@@ -32,12 +32,6 @@ notation `ω^ x` for `of (ω ^ x.val)`. This typeclass will get reused for `IGam
 
 open Ordinal
 
-theorem Ordinal.lt_mul_add_one_iff {x y z : Ordinal} :
-    x < y * (z + 1) ↔ ∃ w < y, x ≤ y * z + w := by
-  obtain rfl | hy := eq_or_ne y 0
-  · simp
-  · rw [mul_add_one, lt_add_iff hy]
-
 /-- A typeclass for the the `ω^` notation. -/
 class Wpow (α : Type*) where
   /-- The `ω`-map, i.e. base `ω` exponentiation. -/

From 9fec5a732f54a5dabf9bfdd4008a56320dee894f Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Wed, 27 May 2026 18:41:53 -0600
Subject: [PATCH 7/9] fix

---
 CombinatorialGames/NatOrdinal/Basic.lean | 2 --
 CombinatorialGames/NatOrdinal/Pow.lean   | 4 ++--
 CombinatorialGames/Nimber/Basic.lean     | 5 -----
 3 files changed, 2 insertions(+), 9 deletions(-)

diff --git a/CombinatorialGames/NatOrdinal/Basic.lean b/CombinatorialGames/NatOrdinal/Basic.lean
index 13c88f44..8ff344e0 100644
--- a/CombinatorialGames/NatOrdinal/Basic.lean
+++ b/CombinatorialGames/NatOrdinal/Basic.lean
@@ -180,8 +180,6 @@ instance : AddMonoidWithOne NatOrdinal where
 @[simp, norm_cast] theorem val_lt_natCast_iff {a : NatOrdinal} {b : ℕ} : val a < b ↔ a < b := .rfl
 @[simp, norm_cast] theorem val_eq_natCast_iff {a : NatOrdinal} {b : ℕ} : val a = b ↔ a = b := .rfl
 
-@[simp] protected theorem succ_one : succ (1 : NatOrdinal) = 2 := one_add_one_eq_two (R := Ordinal)
-
 @[simp]
 theorem natCast_image_Iio (n : ℕ) : Nat.cast '' Iio n = Iio (n : NatOrdinal) :=
   Ordinal.natCast_image_Iio n
diff --git a/CombinatorialGames/NatOrdinal/Pow.lean b/CombinatorialGames/NatOrdinal/Pow.lean
index 8d07bc88..c8d55918 100644
--- a/CombinatorialGames/NatOrdinal/Pow.lean
+++ b/CombinatorialGames/NatOrdinal/Pow.lean
@@ -197,8 +197,8 @@ theorem wpow_add (x y : NatOrdinal) : ω^ (x + y) = ω^ x * ω^ y := by
 termination_by (x, y)
 
 theorem mul_lt_wpow_wpow (hx : x < ω^ ω^ z) (hy : y < ω^ ω^ z) : x * y < ω^ ω^ z := by
-  induction x with | mk x
-  induction y with | mk y
+  cases x with | of x
+  cases y with | of y
   obtain rfl | hz := eq_or_ne z 0
   · simp_rw [wpow_zero, wpow_one, of.lt_iff_lt, Ordinal.lt_omega0] at hx hy
     obtain ⟨m, rfl⟩ := hx
diff --git a/CombinatorialGames/Nimber/Basic.lean b/CombinatorialGames/Nimber/Basic.lean
index 698869b3..5d639ec4 100644
--- a/CombinatorialGames/Nimber/Basic.lean
+++ b/CombinatorialGames/Nimber/Basic.lean
@@ -59,11 +59,6 @@ attribute [simp] succ_zero succ_ne_zero Iio_one lt_one_iff
 @[inherit_doc] scoped prefix:75 "∗" => of
 recommended_spelling "of" for "∗" in [Nimber.«term∗_»]
 
-@[simp] theorem Iio_two : Set.Iio (∗2) = {0, 1} := Order.Iio_two (α := Ordinal)
-theorem lt_two_iff {x : Nimber} : x < ∗2 ↔ x = 0 ∨ x = 1 := Set.ext_iff.1 Iio_two x
-
-@[simp] theorem succ_one : Order.succ 1 = ∗2 := one_add_one_eq_two (R := Ordinal)
-
 theorem not_small_nimber : ¬ Small.{u} Nimber.{u} := not_small_ordinal
 
 /-! ### Nimber addition -/

From cfbd720be716c5d671fc676fa37a729f5152dc8e Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Wed, 27 May 2026 18:43:19 -0600
Subject: [PATCH 8/9] oops

---
 CombinatorialGames/Nimber/Basic.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CombinatorialGames/Nimber/Basic.lean b/CombinatorialGames/Nimber/Basic.lean
index 5d639ec4..698869b3 100644
--- a/CombinatorialGames/Nimber/Basic.lean
+++ b/CombinatorialGames/Nimber/Basic.lean
@@ -59,6 +59,11 @@ attribute [simp] succ_zero succ_ne_zero Iio_one lt_one_iff
 @[inherit_doc] scoped prefix:75 "∗" => of
 recommended_spelling "of" for "∗" in [Nimber.«term∗_»]
 
+@[simp] theorem Iio_two : Set.Iio (∗2) = {0, 1} := Order.Iio_two (α := Ordinal)
+theorem lt_two_iff {x : Nimber} : x < ∗2 ↔ x = 0 ∨ x = 1 := Set.ext_iff.1 Iio_two x
+
+@[simp] theorem succ_one : Order.succ 1 = ∗2 := one_add_one_eq_two (R := Ordinal)
+
 theorem not_small_nimber : ¬ Small.{u} Nimber.{u} := not_small_ordinal
 
 /-! ### Nimber addition -/

From 640cdb2e9e7dc73d0025fa37187ed5b17273d08f Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Thu, 28 May 2026 11:24:07 -0600
Subject: [PATCH 9/9] rename

---
 CombinatorialGames/NatOrdinal/Pow.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CombinatorialGames/NatOrdinal/Pow.lean b/CombinatorialGames/NatOrdinal/Pow.lean
index c8d55918..0cd56a27 100644
--- a/CombinatorialGames/NatOrdinal/Pow.lean
+++ b/CombinatorialGames/NatOrdinal/Pow.lean
@@ -132,7 +132,7 @@ theorem wpow_mul_natCast_lt (h : x < y) (n : ℕ) : ω^ x * n < ω^ y := by
   exact omega0_opow_mul_nat_lt h n
 
 @[simp]
-theorem of_opow_mul_natCast (x : Ordinal) (n : ℕ) : of (ω ^ x * n) = ω^ of x * n := by
+theorem of_omega0_opow_mul_natCast (x : Ordinal) (n : ℕ) : of (ω ^ x * n) = ω^ of x * n := by
   simpa using (wpow_mul_natCast (of x) n).symm
 
 theorem lt_wpow_iff (hx : x ≠ 0) : y < ω^ x ↔ ∃ z < x, ∃ n : ℕ, y < ω^ z * n := by