Lower Lipschitz bound along a prime Reeb orbit

import Definitions.Def_FiniteEnergyPlane_Winding

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- On a prime periodic Reeb orbit, `‖x(τ) - x(τ')‖` is bounded below by a multiple of `|τ - τ'|`
whenever `|τ - τ'| ≤ T / 2`. -/
theorem exists_mul_abs_sub_le_norm_sub_of_isPrime {n : ℕ} (H : V n → ℝ)
    (hH : IsStrictlyStarShapedLevel H) (P : ReebOrbit H) (hP : P.IsPrime) :
    ∃ c > 0, ∀ τ τ' : ℝ, |τ - τ'| ≤ P.T / 2 → c * |τ - τ'| ≤ ‖P.x τ - P.x τ'‖ := by
  sorry

end FiniteEnergyPlane