case pos
n : ℕ
a : ZMod n
h2a : 2 * val a = n
⊢ Int.natAbs (valMinAbs (-a)) = Int.natAbs (valMinAbs a)

case neg
n : ℕ
a : ZMod n
h2a : ¬2 * val a = n
⊢ Int.natAbs (valMinAbs (-a)) = Int.natAbs (valMinAbs a)
n : ℕ
a : ZMod n
⊢ Int.natAbs (valMinAbs (-a)) = Int.natAbs (valMinAbs a)
by_cases h2a : 2 * a.val = n
no goals
case pos
n : ℕ
a : ZMod n
h2a : 2 * val a = n
⊢ Int.natAbs (valMinAbs (-a)) = Int.natAbs (valMinAbs a)
rw [a.neg_eq_self_iff.2 (Or.inr h2a)]
no goals
case neg
n : ℕ
a : ZMod n
h2a : ¬2 * val a = n
⊢ Int.natAbs (valMinAbs (-a)) = Int.natAbs (valMinAbs a)
rw [valMinAbs_neg_of_ne_half h2a, Int.natAbs_neg]