Trace zero tau zero product

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.trace_zero_tau_zero_product {nu : ℤ} (z w : QuadInt 0 nu)
    (hz : 2 * z.re = 0) (hw : 2 * w.re = 0) :
    z * w + 1 = ((1 - nu * z.im * w.im : ℤ) : QuadInt 0 nu) := by sorry















end D1Bound5
end