no goals
α : Type u_1
inst✝ : AddCommGroup α
p a a₁ a₂ b b₁ b₂ c : α
n : ℕ
z : ℤ
x✝ : a₂ ≡ b₂ [PMOD p]
m : ℤ
hm : b₂ - a₂ = m • p
⊢ (∃ b, b₁ + b₂ - (a₁ + a₂) = ↑(Equiv.addRight m).symm.symm b • p) ↔ a₁ ≡ b₁ [PMOD p]
simp [add_sub_add_comm, hm, add_smul, ModEq]