Unit Pair Pell Description — norm lower

import Lean.Elab.Tactic.Omega
import Mathlib.Algebra.Group.Int.Units
import Mathlib.Algebra.Polynomial.Monic
import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Ring.Equiv
import Mathlib.Algebra.Squarefree.Basic
import Mathlib.Analysis.Complex.Norm
import Mathlib.Data.Finset.Card
import Mathlib.Data.Int.GCD
import Mathlib.LinearAlgebra.Dimension.Free
import Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
import Mathlib.NumberTheory.NumberField.Norm
import Mathlib.Tactic.GCongr
import Mathlib.Tactic.IntervalCases
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_FullRingUnitPairPell_Definitions

section
namespace D1Bound5










theorem _root_.D1Bound5.UnitPairPellDescription.norm_lower
    (d : ℤ) (w z : ℂ) (hd : 0 < d) (hw : w*w = -(d : ℂ))
    (h : UnitPairPellDescription d w z) : (d : ℝ)+1 ≤ ‖z‖ := by sorry

open scoped NumberField
open Module



end D1Bound5
end