∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {N : ℕ} {τ : ℝ}
  (a : Besicovitch.SatelliteConfig E N τ) (i j : Fin N.succ),
  i ≠ j →
    (fun i j =>
        (a.r (Fin.last N))⁻¹ * a.r i ≤
              dist ((a.r (Fin.last N))⁻¹ • (a.c i - a.c (Fin.last N)))
                ((a.r (Fin.last N))⁻¹ • (a.c j - a.c (Fin.last N))) ∧
            (a.r (Fin.last N))⁻¹ * a.r j ≤ τ * ((a.r (Fin.last N))⁻¹ * a.r i) ∨
          (a.r (Fin.last N))⁻¹ * a.r j ≤
              dist ((a.r (Fin.last N))⁻¹ • (a.c j - a.c (Fin.last N)))
                ((a.r (Fin.last N))⁻¹ • (a.c i - a.c (Fin.last N))) ∧
            (a.r (Fin.last N))⁻¹ * a.r i ≤ τ * ((a.r (Fin.last N))⁻¹ * a.r j))
      i j