n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ ↑(Int.natAbs (valMinAbs x)) * 2 ≤ ↑n
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ Int.natAbs (valMinAbs x) ≤ n / 2
rw [Nat.le_div_two_iff_mul_two_le]
case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : valMinAbs x = ↑(Int.natAbs (valMinAbs x))
⊢ ↑(Int.natAbs (valMinAbs x)) * 2 ≤ ↑n

case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : valMinAbs x = -↑(Int.natAbs (valMinAbs x))
⊢ ↑(Int.natAbs (valMinAbs x)) * 2 ≤ ↑n
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ ↑(Int.natAbs (valMinAbs x)) * 2 ≤ ↑n
cases' x.valMinAbs.natAbs_eq with h h
case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : valMinAbs x = ↑(Int.natAbs (valMinAbs x))
⊢ valMinAbs x * 2 ≤ ↑n
case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : valMinAbs x = ↑(Int.natAbs (valMinAbs x))
⊢ ↑(Int.natAbs (valMinAbs x)) * 2 ≤ ↑n
rw [← h]
no goals
case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : valMinAbs x = ↑(Int.natAbs (valMinAbs x))
⊢ valMinAbs x * 2 ≤ ↑n
exact x.valMinAbs_mem_Ioc.2
case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : valMinAbs x = -↑(Int.natAbs (valMinAbs x))
⊢ -↑n ≤ valMinAbs x * 2
case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : valMinAbs x = -↑(Int.natAbs (valMinAbs x))
⊢ ↑(Int.natAbs (valMinAbs x)) * 2 ≤ ↑n
rw [← neg_le_neg_iff, ← neg_mul, ← h]
no goals
case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : valMinAbs x = -↑(Int.natAbs (valMinAbs x))
⊢ -↑n ≤ valMinAbs x * 2
exact x.valMinAbs_mem_Ioc.1.le