From the six-point property to the Besicovitch pair condition

This file turns a finite two-color packing theorem into the Besicovitch pair condition.

theorem LeanPool.Besicovitch.SixPointFiniteProperty.besicovitchPairCondition {s beta : ℝ} (hs : 0 < s) (hsbeta : s < beta) (hfinite : SixPointFiniteProperty s) : BesicovitchPairCondition beta

The finite six-point property at s implies the Besicovitch pair condition above s.