English
Let α be an ordered additive group with Archimedean property and p > 0. For any a, b in α, the interval modulo p from a to a + p and the complementary interval from b to b − p are interconnected by a single equality: the IcoMod value of a − b equals p minus the IocMod value of b − a.
Русский
Пусть α — упорядоченная аддитивная группа с Архимедовым свойством и p > 0. При любых a, b ∈ α равенство между интервалами по модулю p: значение IcoMod для a − b равно p минус значение IocMod для b − a.
LaTeX
$$$$ \operatorname{toIcoMod}(hp, 0, a-b) = p - \operatorname{toIocMod}(hp, 0, b-a) $$$$
Lean4
theorem toIcoMod_zero_sub_comm (a b : α) : toIcoMod hp 0 (a - b) = p - toIocMod hp 0 (b - a) := by
rw [← neg_sub, toIcoMod_neg, neg_zero]
