English
For fixed a and p > 0, the equality toIocMod hp a b = toIocMod hp a c holds iff there exists an integer n with c − b = n · p.
Русский
Для фиксированных a и p > 0 равенство toIocMod hp a b = toIocMod hp a c эквивалентно существованию целого числа n, такого что c − b = n · p.
LaTeX
$$$ toIocMod hp a b = toIocMod hp a c \\iff ∃ n : \\mathbb{Z},\\ c - b = n \\cdot p $$$
Lean4
theorem toIocMod_eq_toIocMod : toIocMod hp a b = toIocMod hp a c ↔ ∃ n : ℤ, c - b = n • p :=
by
refine ⟨fun h => ⟨toIocDiv hp a c - toIocDiv hp a b, ?_⟩, fun h => ?_⟩
· conv_lhs => rw [← toIocMod_add_toIocDiv_zsmul hp a b, ← toIocMod_add_toIocDiv_zsmul hp a c]
rw [h, sub_smul]
abel
· rcases h with ⟨z, hz⟩
rw [sub_eq_iff_eq_add] at hz
rw [hz, toIocMod_zsmul_add]
