∀ {E : Type u_1} [inst : NormedAddCommGroup E] (x x_1 : E)
  (motive :
    (∃ δ, 0 < δ ∧ ∀ ⦃x_2 : E⦄, ‖x_2‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ‖x - x_1‖ ≤ ‖x_2 - y‖ → ‖x_2 + y‖ ≤ 2 - δ) → Prop)
  (x_2 : ∃ δ, 0 < δ ∧ ∀ ⦃x_2 : E⦄, ‖x_2‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ‖x - x_1‖ ≤ ‖x_2 - y‖ → ‖x_2 + y‖ ≤ 2 - δ),
  (∀ (w : ℝ) (hδ : 0 < w) (h : ∀ ⦃x_3 : E⦄, ‖x_3‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ‖x - x_1‖ ≤ ‖x_3 - y‖ → ‖x_3 + y‖ ≤ 2 - w),
      motive ⋯) →
    motive x_2