English
Let p be a fixed modulus in an additive abelian group. If a₂ ≡ b₂ (mod p), then for any a₁ and b₁ we have a₁ + a₂ ≡ b₁ + b₂ (mod p) if and only if a₁ ≡ b₁ (mod p).
Русский
Пусть p фиксированное по модулю в аддитивной абелевой группе. Если a₂ ≡ b₂ (mod p), то для любых a₁ и b₁ верно: a₁ + a₂ ≡ b₁ + b₂ (mod p) тогда и только тогда, когда a₁ ≡ b₁ (mod p).
LaTeX
$$$ a_2 \\equiv b_2 \\pmod{p} \\; \\Rightarrow\\; \\big( a_1 + a_2 \\equiv b_1 + b_2 \\pmod{p} \\ \\iff\\; a_1 \\equiv b_1 \\pmod{p} \\big) $$$
Lean4
@[simp]
protected theorem add_iff_right : a₂ ≡ b₂ [PMOD p] → (a₁ + a₂ ≡ b₁ + b₂ [PMOD p] ↔ a₁ ≡ b₁ [PMOD p]) := fun ⟨m, hm⟩ =>
(Equiv.addRight m).symm.exists_congr_left.trans <| by simp [add_sub_add_comm, hm, add_smul, ModEq]
