English
The sum modulo c distributes over addition with a conditional carrying term: (a+b) mod c equals a mod c plus b mod c in the appropriate form; equivalently, (a+b) mod c = (a mod c + b mod c) mod c.
Русский
Сумма по модулю c распределяется по сложению с условной «перекладкой»: (a+b) mod c = (a mod c + b mod c) mod c.
LaTeX
$$$\\\\forall a,b,c \\\\in \\\\mathbb{N},\\\\ (a+b) \\\\bmod c = (a \\\\bmod c + b \\\\bmod c) \\\\bmod c$$$
Lean4
theorem add_mod_add_ite (a b c : ℕ) : ((a + b) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c :=
have : (a + b) % c = (a % c + b % c) % c := ((mod_modEq _ _).add <| mod_modEq _ _).symm
if hc0 : c = 0 then by simp [hc0, Nat.mod_zero]
else by
rw [this]
split_ifs with h
· have h2 : (a % c + b % c) / c < 2 :=
Nat.div_lt_of_lt_mul
(by
rw [mul_two]
exact add_lt_add (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0)) (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0)))
have h0 : 0 < (a % c + b % c) / c := Nat.div_pos h (Nat.pos_of_ne_zero hc0)
rw [← @add_right_cancel_iff _ _ _ (c * ((a % c + b % c) / c)), add_comm _ c, add_assoc, mod_add_div,
le_antisymm (le_of_lt_succ h2) h0, mul_one, add_comm]
· rw [Nat.mod_eq_of_lt (lt_of_not_ge h), add_zero]
