congr
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
this : OneHom.toFun (↑↑inclusion) b * (OneHom.toFun (↑↑inclusion) b)⁻¹ = 1
⊢ OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹ -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) =
    OneHom.toFun (↑↑inclusion) a * sorryAx ℂ true -
      OneHom.toFun (↑↑inclusion) b *
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) *
        sorryAx ℂ true
case e_a.e_a
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
this : OneHom.toFun (↑↑inclusion) b * (OneHom.toFun (↑↑inclusion) b)⁻¹ = 1
⊢ (OneHom.toFun (↑↑inclusion) b)⁻¹ = sorryAx ℂ true

case e_a
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
this : OneHom.toFun (↑↑inclusion) b * (OneHom.toFun (↑↑inclusion) b)⁻¹ = 1
⊢ OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) =
    OneHom.toFun (↑↑inclusion) b *
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) *
      sorryAx ℂ true