{α : Type u_1} →
  [inst : MetricSpace α] →
    {N : ℕ} →
      {τ : ℝ} →
        {motive : Besicovitch.SatelliteConfig α N τ → Sort u} →
          ((c : Fin N.succ → α) →
              (r : Fin N.succ → ℝ) →
                (rpos : ∀ (i : Fin N.succ), 0 < r i) →
                  (h :
                      Pairwise fun i j =>
                        r i ≤ dist (c i) (c j) ∧ r j ≤ τ * r i ∨ r j ≤ dist (c j) (c i) ∧ r i ≤ τ * r j) →
                    (hlast : ∀ i < Fin.last N, r i ≤ dist (c i) (c (Fin.last N)) ∧ r (Fin.last N) ≤ τ * r i) →
                      (inter : ∀ i < Fin.last N, dist (c i) (c (Fin.last N)) ≤ r i + r (Fin.last N)) →
                        motive { c := c, r := r, rpos := rpos, h := h, hlast := hlast, inter := inter }) →
            (t : Besicovitch.SatelliteConfig α N τ) → motive t