mod_sub_of_le — Mathlib

English

Let a, b, n be natural numbers with b ≤ a mod n. Then a mod n − b = (a − b) mod n.

Русский

Пусть a, b, n — естественные числа и b ≤ a mod n. Тогда a mod n − b = (a − b) mod n.

LaTeX

$$$ b \le a \bmod n \Rightarrow a \bmod n - b = (a - b) \bmod n $$$

Lean4

theorem mod_sub_of_le {a b n : ℕ} (h : b ≤ a % n) : a % n - b = (a - b) % n :=
  by
  rcases n.eq_zero_or_pos with rfl | hn; · simp only [mod_zero]
  nth_rw 2 [← div_add_mod a n]; rw [Nat.add_sub_assoc h, mul_add_mod]
  exact (mod_eq_of_lt <| (sub_le ..).trans_lt (mod_lt a hn)).symm

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