no goals
α : Type u_1
inst✝¹ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
inst✝ : NoZeroSMulDivisors ℤ α
hn : z ≠ 0
m : ℤ
⊢ z • b - z • a = m • z • p ↔ b - a = m • p
rw [← smul_sub, smul_comm, smul_right_inj hn]