Quad Int eq int Cast of im eq zero

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Data.Int.Sqrt
import Mathlib.Tactic.Linarith
import Definitions.Def_D1Bound5_Coordinates_Definitions

section
namespace D1Bound5


theorem _root_.D1Bound5.quadInt_eq_intCast_of_im_eq_zero {tau nu : ℤ}
    (z : QuadInt tau nu) (him : z.im = 0) :
    z = (z.re : QuadInt tau nu) := by sorry









end D1Bound5
end