add_left_cancel — Mathlib

English

If a ≡ b (mod n) and a + c ≡ b + d (mod n), then c ≡ d (mod n).

Русский

Если a ≡ b (mod n) и a + c ≡ b + d (mod n), тогда c ≡ d (mod n).

LaTeX

$$$a \\equiv b \\pmod{n} \\land a + c \\equiv b + d \\pmod{n} \\Rightarrow c \\equiv d \\pmod{n}$$$

Lean4

protected theorem add_left_cancel (h₁ : a ≡ b [MOD n]) (h₂ : a + c ≡ b + d [MOD n]) : c ≡ d [MOD n] :=
  by
  simp only [modEq_iff_dvd, Int.natCast_add] at *
  rw [add_sub_add_comm] at h₂
  convert Int.dvd_sub h₂ h₁ using 1
  rw [add_sub_cancel_left]

Похожие утверждения