One three common extension is integer

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Definitions.Def_D1Bound5_Coordinates_Definitions

section
namespace D1Bound5









theorem _root_.D1Bound5.one_three_common_extension_is_integer (tau nu : ℤ)
    (hd : 0 < QuadInt.discriminant tau nu) {z : QuadInt tau nu}
    (hr : ∃ r, r*r = z+1) (hs : ∃ s, s*s = 3*z+1) :
    ∃ n : ℤ, z = (n : QuadInt tau nu) := by sorry

end D1Bound5
end