add_right_cancel — Mathlib

English

Let n, a, b, c, d be natural numbers. If c ≡ d (mod n) and a + c ≡ b + d (mod n), then a ≡ b (mod n).

Русский

Пусть n, a, b, c, d — натуральные числа. Если c ≡ d (mod n) и a + c ≡ b + d (mod n), то a ≡ b (mod n).

LaTeX

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

Lean4

protected theorem add_right_cancel (h₁ : c ≡ d [MOD n]) (h₂ : a + c ≡ b + d [MOD n]) : a ≡ b [MOD n] :=
  by
  rw [add_comm a, add_comm b] at h₂
  exact h₁.add_left_cancel h₂

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