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