no goals
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
b c : α
⊢ ∃! x, b - ↑(Equiv.neg ℤ) x • a ∈ Ioc c (c + a)
simpa only [Equiv.neg_apply, neg_zsmul, sub_neg_eq_add] using
  existsUnique_add_zsmul_mem_Ioc ha b c