English
Let n ∈ ℕ and x,y ∈ ℤ with x ≡ y (mod n) and |x| ≤ n/2. Then |x| ≤ |y|.
Русский
Пусть n ∈ ℕ и x,y ∈ ℤ такие, что x ≡ y (mod n) и |x| ≤ n/2. Тогда |x| ≤ |y|.
LaTeX
$$$ x.natAbs \le y.natAbs \quad\text{whenever } (x : \mathbb{Z}/n\mathbb{Z}) = y \\mathrm{cast}, \; x.natAbs \le \frac{n}{2} $$$
Lean4
theorem natAbs_min_of_le_div_two (n : ℕ) (x y : ℤ) (he : (x : ZMod n) = y) (hl : x.natAbs ≤ n / 2) :
x.natAbs ≤ y.natAbs := by
rw [intCast_eq_intCast_iff_dvd_sub] at he
obtain ⟨m, he⟩ := he
rw [sub_eq_iff_eq_add] at he
subst he
obtain rfl | hm := eq_or_ne m 0
· rw [mul_zero, zero_add]
apply hl.trans
rw [← add_le_add_iff_right x.natAbs]
refine le_trans (le_trans ((add_le_add_iff_left _).2 hl) ?_) (Int.natAbs_sub_le _ _)
rw [add_sub_cancel_right, Int.natAbs_mul, Int.natAbs_natCast]
refine le_trans ?_ (Nat.le_mul_of_pos_right _ <| Int.natAbs_pos.2 hm)
rw [← mul_two]; apply Nat.div_mul_le_self
