no goals
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
b c : α
⊢ ∃! m, b - m • a ∈ Ico c (c + a)
simpa only [mem_Ico, le_sub_iff_add_le, zero_add, add_comm c, sub_lt_iff_lt_add', add_assoc] using
  existsUnique_zsmul_near_of_pos' ha (b - c)