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