n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑(val a) - ↑n ≤ 0
⊢ ↑(Int.natAbs (valMinAbs a)) = if val a ≤ n / 2 then a else -a
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑(Int.natAbs (valMinAbs a)) = if val a ≤ n / 2 then a else -a
have : (a.val : ℤ) - n ≤ 0 := by
  erw [sub_nonpos, Int.ofNat_le]
  exact a.val_le
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑(val a) - ↑n ≤ 0
⊢ ↑(Int.natAbs (if val a ≤ n / 2 then ↑(val a) else ↑(val a) - ↑n)) = if val a ≤ n / 2 then a else -a
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑(val a) - ↑n ≤ 0
⊢ ↑(Int.natAbs (valMinAbs a)) = if val a ≤ n / 2 then a else -a
rw [valMinAbs_def_pos]
case inl
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑(val a) - ↑n ≤ 0
h✝ : val a ≤ n / 2
⊢ ↑(Int.natAbs ↑(val a)) = a

case inr
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑(val a) - ↑n ≤ 0
h✝ : ¬val a ≤ n / 2
⊢ ↑(Int.natAbs (↑(val a) - ↑n)) = -a
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑(val a) - ↑n ≤ 0
⊢ ↑(Int.natAbs (if val a ≤ n / 2 then ↑(val a) else ↑(val a) - ↑n)) = if val a ≤ n / 2 then a else -a
split_ifs
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ val a ≤ n
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑(val a) - ↑n ≤ 0
erw [sub_nonpos, Int.ofNat_le]
no goals
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ val a ≤ n
exact a.val_le
no goals
case inl
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑(val a) - ↑n ≤ 0
h✝ : val a ≤ n / 2
⊢ ↑(Int.natAbs ↑(val a)) = a
rw [Int.natAbs_ofNat, nat_cast_zmod_val]
no goals
case inr
n : ℕ
inst✝ : NeZero n
a : ZMod n
this : ↑(val a) - ↑n ≤ 0
h✝ : ¬val a ≤ n / 2
⊢ ↑(Int.natAbs (↑(val a) - ↑n)) = -a
rw [← Int.cast_ofNat, Int.ofNat_natAbs_of_nonpos this, Int.cast_neg, Int.cast_sub,
  Int.cast_ofNat, Int.cast_ofNat, nat_cast_self, sub_zero, nat_cast_zmod_val]