English
For [NeZero n], each x ∈ ZMod n satisfies x.valMinAbs * 2 ∈ (-n, n], i.e., -n < 2 x.valMinAbs ≤ n.
Русский
Для [NeZero n] для любого x ∈ ZMod n выполняется x.valMinAbs · 2 ∈ (-n, n], то есть -n < 2·x.valMinAbs ≤ n.
LaTeX
$$$[\\mathrm{NeZero}\\ n]\\ (x : \\mathbb{Z}/n\\mathbb{Z})\\ x.valMinAbs \\cdot 2 \\in (-n, n]$$
Lean4
theorem valMinAbs_mem_Ioc [NeZero n] (x : ZMod n) : x.valMinAbs * 2 ∈ Set.Ioc (-n : ℤ) n :=
by
simp_rw [valMinAbs_def_pos, Nat.le_div_two_iff_mul_two_le]; split_ifs with h
· refine ⟨(neg_lt_zero.2 <| mod_cast NeZero.pos n).trans_le (mul_nonneg ?_ ?_), h⟩
exacts [Nat.cast_nonneg _, zero_le_two]
· refine ⟨?_, le_trans (mul_nonpos_of_nonpos_of_nonneg ?_ zero_le_two) <| Nat.cast_nonneg _⟩
· linarith only [h]
· rw [sub_nonpos, Int.ofNat_le]
exact x.val_lt.le
