English
If c ≤ a ⇔ d ≤ b, a ≡ b (mod n) and c ≡ d (mod n), then a − c ≡ b − d (mod n).
Русский
Если c ≤ a ⇔ d ≤ b, a ≡ b (mod n) и c ≡ d (mod n), то a − c ≡ b − d (mod n).
LaTeX
$$$ (c \le a \Leftrightarrow d \le b) \land (a \equiv b \pmod{n}) \land (c \equiv d \pmod{n}) \Rightarrow a - c \equiv b - d \pmod{n} $$$
Lean4
protected theorem sub' (h : c ≤ a ↔ d ≤ b) (hab : a ≡ b [MOD n]) (hcd : c ≡ d [MOD n]) : a - c ≡ b - d [MOD n] :=
by
obtain hac | hca := lt_or_ge a c
· rw [Nat.sub_eq_zero_of_le hac.le, Nat.sub_eq_zero_of_le ((lt_iff_lt_of_le_iff_le h).1 hac).le]
rw [modEq_iff_dvd, Int.natCast_sub hca, Int.natCast_sub <| h.1 hca, sub_sub_sub_comm]
exact Int.dvd_sub hab.dvd hcd.dvd
