Carries in addition modulo a natural number

This file records the elementary identity equating the carries produced by the two associations of a sum of three natural numbers modulo n.

Main results

• TauCeti.Nat.carry_add_carry: the two ways to associate a three-term sum produce the same total number of carries.

theorem TauCeti.Nat.carry_add_carry {n i j k : ℕ} (hi : i < n) (hj : j < n) (hk : k < n) : ((if n ≤ (i + j) % n + k then 1 else 0) + if n ≤ i + j then 1 else 0) = (if n ≤ j + k then 1 else 0) + if n ≤ i + (j + k) % n then 1 else 0

The carries of (i + j) + k and of i + (j + k) modulo n agree: both count the multiples of n in i + j + k.