n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ (if ↑(val x) * 2 ≤ ↑n then ↑(val x) else ↑(val x) - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ valMinAbs x * 2 ∈ Set.Ioc (-↑n) ↑n
simp_rw [valMinAbs_def_pos, Nat.le_div_two_iff_mul_two_le]
case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑(val x) * 2 ≤ ↑n
⊢ ↑(val x) * 2 ∈ Set.Ioc (-↑n) ↑n

case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑(val x) * 2 ≤ ↑n
⊢ (↑(val x) - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ (if ↑(val x) * 2 ≤ ↑n then ↑(val x) else ↑(val x) - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n
split_ifs with h
case inl.refine'_1
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑(val x) * 2 ≤ ↑n
⊢ 0 ≤ ↑(val x)

case inl.refine'_2
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑(val x) * 2 ≤ ↑n
⊢ 0 ≤ 2
case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑(val x) * 2 ≤ ↑n
⊢ ↑(val x) * 2 ∈ Set.Ioc (-↑n) ↑n
refine' ⟨(neg_lt_zero.2 <| by exact_mod_cast NeZero.pos n).trans_le (mul_nonneg _ _), h⟩
no goals
case inl.refine'_1
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑(val x) * 2 ≤ ↑n
⊢ 0 ≤ ↑(val x)

case inl.refine'_2
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑(val x) * 2 ≤ ↑n
⊢ 0 ≤ 2
exacts [Nat.cast_nonneg _, zero_le_two]
no goals
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ↑(val x) * 2 ≤ ↑n
⊢ 0 < ↑n
exact_mod_cast NeZero.pos n
case inr.refine'_1
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑(val x) * 2 ≤ ↑n
⊢ -↑n < (↑(val x) - ↑n) * 2

case inr.refine'_2
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑(val x) * 2 ≤ ↑n
⊢ ↑(val x) - ↑n ≤ 0
case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑(val x) * 2 ≤ ↑n
⊢ (↑(val x) - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n
refine' ⟨_, le_trans (mul_nonpos_of_nonpos_of_nonneg _ zero_le_two) <| Nat.cast_nonneg _⟩
no goals
case inr.refine'_1
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑(val x) * 2 ≤ ↑n
⊢ -↑n < (↑(val x) - ↑n) * 2
linarith only [h]
case inr.refine'_2
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑(val x) * 2 ≤ ↑n
⊢ val x ≤ n
case inr.refine'_2
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑(val x) * 2 ≤ ↑n
⊢ ↑(val x) - ↑n ≤ 0
rw [sub_nonpos, Int.ofNat_le]
no goals
case inr.refine'_2
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑(val x) * 2 ≤ ↑n
⊢ val x ≤ n
exact x.val_lt.le