n✝ a n : ℕ
x y : ℤ
he : ↑n ∣ y - x
hl : Int.natAbs x ≤ n / 2
⊢ Int.natAbs x ≤ Int.natAbs y
n✝ a n : ℕ
x y : ℤ
he : ↑x = ↑y
hl : Int.natAbs x ≤ n / 2
⊢ Int.natAbs x ≤ Int.natAbs y
rw [int_cast_eq_int_cast_iff_dvd_sub] at he
case intro
n✝ a n : ℕ
x y : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
he : y - x = ↑n * m
⊢ Int.natAbs x ≤ Int.natAbs y
n✝ a n : ℕ
x y : ℤ
he : ↑n ∣ y - x
hl : Int.natAbs x ≤ n / 2
⊢ Int.natAbs x ≤ Int.natAbs y
obtain ⟨m, he⟩ := he
case intro
n✝ a n : ℕ
x y : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
he : y = ↑n * m + x
⊢ Int.natAbs x ≤ Int.natAbs y
case intro
n✝ a n : ℕ
x y : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
he : y - x = ↑n * m
⊢ Int.natAbs x ≤ Int.natAbs y
rw [sub_eq_iff_eq_add] at he
case intro
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
⊢ Int.natAbs x ≤ Int.natAbs (↑n * m + x)
case intro
n✝ a n : ℕ
x y : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
he : y = ↑n * m + x
⊢ Int.natAbs x ≤ Int.natAbs y
subst he
case intro.inl
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
⊢ Int.natAbs x ≤ Int.natAbs (↑n * 0 + x)

case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ Int.natAbs x ≤ Int.natAbs (↑n * m + x)
case intro
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
⊢ Int.natAbs x ≤ Int.natAbs (↑n * m + x)
obtain rfl | hm := eq_or_ne m 0
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 ≤ Int.natAbs (↑n * m + x)
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ Int.natAbs x ≤ Int.natAbs (↑n * m + x)
apply hl.trans
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + Int.natAbs x ≤ Int.natAbs (↑n * m + x) + Int.natAbs x
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 ≤ Int.natAbs (↑n * m + x)
rw [← add_le_add_iff_right x.natAbs]
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ Int.natAbs (↑n * m + x - x)
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + Int.natAbs x ≤ Int.natAbs (↑n * m + x) + Int.natAbs x
refine' le_trans (le_trans ((add_le_add_iff_left _).2 hl) _) (Int.natAbs_sub_le _ _)
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ n * Int.natAbs m
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ Int.natAbs (↑n * m + x - x)
rw [add_sub_cancel, Int.natAbs_mul, Int.natAbs_ofNat]
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ n
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ n * Int.natAbs m
refine' le_trans _ (Nat.le_mul_of_pos_right <| Int.natAbs_pos.2 hm)
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 * 2 ≤ n
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 + n / 2 ≤ n
rw [← mul_two]
no goals
case intro.inr
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
m : ℤ
hm : m ≠ 0
⊢ n / 2 * 2 ≤ n
apply Nat.div_mul_le_self
no goals
case intro.inl
n✝ a n : ℕ
x : ℤ
hl : Int.natAbs x ≤ n / 2
⊢ Int.natAbs x ≤ Int.natAbs (↑n * 0 + x)
rw [MulZeroClass.mul_zero, zero_add]