English
For hp, a, b, c, we have toIocMod(hp, a, b) = c iff c ∈ Ioc(a, a+p) and there exists z ∈ ℤ with b = c + z p.
Русский
Для hp, a, b, c выполняется: toIocMod(hp, a, b) = c тогда и только тогда c ∈ Ioc(a, a+p) и существует z ∈ ℤ: b = c + z p.
LaTeX
$$$$\text{toIocMod}(hp, a, b) = c \iff c \in \mathrm{Ioc}(a, a+p) \land \exists z \in \mathbb{Z},\; b = c + z p$$$$
Lean4
theorem toIocMod_eq_iff : toIocMod hp a b = c ↔ c ∈ Set.Ioc a (a + p) ∧ ∃ z : ℤ, b = c + z • p :=
by
refine ⟨fun h => ⟨h ▸ toIocMod_mem_Ioc hp a b, toIocDiv hp a b, h ▸ (toIocMod_add_toIocDiv_zsmul hp _ _).symm⟩, ?_⟩
simp_rw [← @sub_eq_iff_eq_add]
rintro ⟨hc, n, rfl⟩
rw [← toIocDiv_eq_of_sub_zsmul_mem_Ioc hp hc, toIocMod]
