no goals
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n✝ : ℕ
z : ℤ
x✝¹ : a ≡ b [PMOD p]
x✝ : b ≡ c [PMOD p]
m : ℤ
hm : b - a = m • p
n : ℤ
hn : c - b = n • p
⊢ c - a = (m + n) • p
simp [add_smul, ← hm, ← hn]