rw [← QuotientAddGroup.mk_nsmul, nsmul_eq_mul, Ne.def, QuotientAddGroup.eq_zero_iff,
  AddSubgroup.mem_zmultiples_iff, not_exists]
case refine'_2
n : ℕ
hn : 0 < n
⊢ n • ↑(1 / (2 * ↑n)) ≠ 0
case refine'_2
n : ℕ
hn : 0 < n
⊢ ∀ (x : ℤ), ¬x • 1 = ↑n * (1 / (2 * ↑n))