∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Ring β] {abv : β → α} {f g : ℕ → β} (w : α)
  (motive : (∃ i, ∀ j ≥ i, (∀ k ≥ j, abv (f k - f j) < w) ∧ ∀ k ≥ j, abv (g k - g j) < w) → Prop)
  (x : ∃ i, ∀ j ≥ i, (∀ k ≥ j, abv (f k - f j) < w) ∧ ∀ k ≥ j, abv (g k - g j) < w),
  (∀ (i : ℕ) (H : ∀ j ≥ i, (∀ k ≥ j, abv (f k - f j) < w) ∧ ∀ k ≥ j, abv (g k - g j) < w), motive ⋯) → motive x