trunk late geometry

import Definitions.Def_Freiman_trunkGeometry
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.Linarith

open Freiman

theorem Freiman.trunk_late_geometry (t : ℝ) (p : LowerPair) (hs : lowerState t p) (hd : ¬ lowerMixed p ∧ ¬ lowerA p 3 ∧ ¬ lowerA p 9 ∧ lowerL p ∧ ¬ lowerLStar p) :
    ∃ plan : TrunkPlan, TrunkGeometry p plan ∧ ([2],[2]) ∈ plan.labels ∧ ([2],[1]) ∈ plan.labels := by
  sorry