Eisenstein trace zero compatible opposite

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Ring.Equiv
import Mathlib.Data.Finset.Card
import Mathlib.Data.Int.Sqrt
import Mathlib.Tactic.Linarith
import Definitions.Def_D1Bound5_Coordinates_Definitions

section
namespace D1Bound5






theorem _root_.D1Bound5.eisenstein_trace_zero_compatible_opposite
    (z w : QuadInt 1 1) (hz0 : z ≠ 0) (hw0 : w ≠ 0)
    (hz : 2 * z.re + z.im = 0) (hw : 2 * w.re + w.im = 0)
    (hsquare : ∃ r : QuadInt 1 1, r * r = z * w + 1) :
    z.re * w.re < 0 := by sorry





end D1Bound5
end