rw [mul_comm]
case h
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
⊢ d = r * k
case h
s : SelbergSieve
k d m : ℕ
hmd : m.Coprime d
hk : k ≠ 0
r : ℕ
hr : d = k * r
⊢ d = k * r