-- Mathlib/Data/ZMod/Basic.lean
theorem natAbs_min_of_le_div_two (n : ℕ) (x y : ℤ) (he : (x : ZMod n) = y) (hl : x.natAbs ≤ n / 2) :
    x.natAbs ≤ y.natAbs

Proof state:
case intro.inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ (↑n * m + x - x).natAbs

Tactic:
rw [add_sub_cancel_right, Int.natAbs_mul, Int.natAbs_ofNat]

Result:
case intro.inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ n * m.natAbs

Proof state:
case intro
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
⊢ x.natAbs ≤ (↑n * m + x).natAbs

Tactic:
obtain rfl | hm := eq_or_ne m 0

Result:
case intro.inl
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ (↑n * 0 + x).natAbs

case intro.inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ x.natAbs ≤ (↑n * m + x).natAbs

Proof state:
case intro
n : ℕ
x y : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
he : y = ↑n * m + x
⊢ x.natAbs ≤ y.natAbs

Tactic:
subst he

Result:
case intro
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
⊢ x.natAbs ≤ (↑n * m + x).natAbs

Proof state:
case intro.inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 * 2 ≤ n

Tactic:
apply Nat.div_mul_le_self

Result:
no goals

Proof state:
case intro.inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ n * m.natAbs

Tactic:
refine le_trans ?_ (Nat.le_mul_of_pos_right _ <| Int.natAbs_pos.2 hm)

Result:
case intro.inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ n

Proof state:
case intro.inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ n

Tactic:
rw [← mul_two]

Result:
case intro.inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 * 2 ≤ n

Proof state:
case intro.inl
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ (↑n * 0 + x).natAbs

Tactic:
rw [mul_zero, zero_add]

Result:
no goals

Proof state:
case intro
n : ℕ
x y : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
he : y - x = ↑n * m
⊢ x.natAbs ≤ y.natAbs

Tactic:
rw [sub_eq_iff_eq_add] at he

Result:
case intro
n : ℕ
x y : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
he : y = ↑n * m + x
⊢ x.natAbs ≤ y.natAbs

Proof state:
n : ℕ
x y : ℤ
he : ↑x = ↑y
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ y.natAbs

Tactic:
rw [intCast_eq_intCast_iff_dvd_sub] at he

Result:
n : ℕ
x y : ℤ
he : ↑n ∣ y - x
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ y.natAbs

Proof state:
n : ℕ
x y : ℤ
he : ↑n ∣ y - x
hl : x.natAbs ≤ n / 2
⊢ x.natAbs ≤ y.natAbs

Tactic:
obtain ⟨m, he⟩ := he

Result:
case intro
n : ℕ
x y : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
he : y - x = ↑n * m
⊢ x.natAbs ≤ y.natAbs

Proof state:
case intro.inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + x.natAbs ≤ (↑n * m + x).natAbs + x.natAbs

Tactic:
refine le_trans (le_trans ((add_le_add_iff_left _).2 hl) ?_) (Int.natAbs_sub_le _ _)

Result:
case intro.inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ (↑n * m + x - x).natAbs

Proof state:
case intro.inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 ≤ (↑n * m + x).natAbs

Tactic:
rw [← add_le_add_iff_right x.natAbs]

Result:
case intro.inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + x.natAbs ≤ (↑n * m + x).natAbs + x.natAbs

Proof state:
case intro.inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ x.natAbs ≤ (↑n * m + x).natAbs

Tactic:
apply hl.trans

Result:
case intro.inr
n : ℕ
x : ℤ
hl : x.natAbs ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 ≤ (↑n * m + x).natAbs