no goals
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
⊢ ∃! k, 0 ≤ g - k • a ∧ g - k • a < a
simpa only [sub_nonneg, add_zsmul, one_zsmul, sub_lt_iff_lt_add'] using
  existsUnique_zsmul_near_of_pos ha g