English
For any n, a, the equality a.valMinAbs * 2 = n holds if and only if 2 * a.val = n (when n > 0).
Русский
Для любого n и элемента a: ZMod n верно, что a.valMinAbs · 2 = n тогда и только тогда, когда 2·a.val = n (при n > 0).
LaTeX
$$$(a.valMinAbs) \\cdot 2 = n \\;\\iff\\; 2 \\cdot a.val = n$$$
Lean4
theorem valMinAbs_mul_two_eq_iff (a : ZMod n) : a.valMinAbs * 2 = n ↔ 2 * a.val = n :=
by
rcases n with - | n
· simp
by_cases h : a.val ≤ n.succ / 2
· dsimp [valMinAbs]
rw [if_pos h, ← Int.natCast_inj, Nat.cast_mul, Nat.cast_two, mul_comm, Int.natCast_add, Nat.cast_one]
apply iff_of_false _ (mt _ h)
· intro he
rw [← a.valMinAbs_nonneg_iff, ← mul_nonneg_iff_left_nonneg_of_pos, he] at h
exacts [h (Nat.cast_nonneg _), zero_lt_two]
· rw [mul_comm]
exact fun h => (Nat.le_div_iff_mul_le zero_lt_two).2 h.le
