n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ (0 ≤ if val x ≤ n / 2 then ↑(val x) else ↑(val x) - ↑n) ↔ val x ≤ n / 2
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ 0 ≤ valMinAbs x ↔ val x ≤ n / 2
rw [valMinAbs_def_pos]
case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : val x ≤ n / 2
⊢ 0 ≤ ↑(val x) ↔ val x ≤ n / 2

case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬val x ≤ n / 2
⊢ 0 ≤ ↑(val x) - ↑n ↔ val x ≤ n / 2
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ (0 ≤ if val x ≤ n / 2 then ↑(val x) else ↑(val x) - ↑n) ↔ val x ≤ n / 2
split_ifs with h
no goals
case inl
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : val x ≤ n / 2
⊢ 0 ≤ ↑(val x) ↔ val x ≤ n / 2
exact iff_of_true (Nat.cast_nonneg _) h
no goals
case inr
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬val x ≤ n / 2
⊢ 0 ≤ ↑(val x) - ↑n ↔ val x ≤ n / 2
exact iff_of_false (sub_lt_zero.2 <| Int.ofNat_lt.2 x.val_lt).not_le h