One Small Thirds 14 complete

import Mathlib.Algebra.QuadraticAlgebra.Basic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Ring.Equiv
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Prod
import Mathlib.Data.Int.Interval
import Mathlib.Data.Int.Sqrt
import Mathlib.Data.List.Range
import Mathlib.Tactic.IntervalCases
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Definitions.Def_D1Bound5_Coordinates_Definitions
import Definitions.Def_D1Bound5_OneSmallThirdData_Definitions_001
import Definitions.Def_D1Bound5_PairExtensionCore_Definitions

section
namespace D1Bound5
open QuadInt
set_option maxRecDepth 32768
set_option maxHeartbeats 12000000























































































































theorem _root_.D1Bound5.oneSmallThirds_14_complete (s : QuadInt 1 1) (hbound : s.norm ≤ 224)
    (horder : oneSmallPairB_14.norm ≤ s.norm)
    (ha : s ≠ oneSmallPairA_14) (hb : s ≠ oneSmallPairB_14)
    (hpair : PairExtension oneSmallPairA_14 oneSmallPairB_14 s) : s ∈ oneSmallThirds_14 := by sorry









































































































































































































end D1Bound5
end