case inl
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
h : n = 0
⊢ valMinAbs (-a) = -valMinAbs a

case inr
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
h : NeZero n
⊢ valMinAbs (-a) = -valMinAbs a
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
⊢ valMinAbs (-a) = -valMinAbs a
cases' eq_zero_or_neZero n with h h
case inr.refine'_1
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
h : NeZero n
⊢ -a = ↑(-valMinAbs a)

case inr.refine'_2
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
h : NeZero n
⊢ -↑n < -valMinAbs a * 2

case inr.refine'_3
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
h : NeZero n
⊢ -valMinAbs a * 2 ≤ ↑n
case inr
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
h : NeZero n
⊢ valMinAbs (-a) = -valMinAbs a
refine' (valMinAbs_spec _ _).2 ⟨_, _, _⟩
case inl
a : ZMod 0
ha : 2 * val a ≠ 0
⊢ valMinAbs (-a) = -valMinAbs a
case inl
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
h : n = 0
⊢ valMinAbs (-a) = -valMinAbs a
subst h
no goals
case inl
a : ZMod 0
ha : 2 * val a ≠ 0
⊢ valMinAbs (-a) = -valMinAbs a
rfl
no goals
case inr.refine'_1
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
h : NeZero n
⊢ -a = ↑(-valMinAbs a)
rw [Int.cast_neg, coe_valMinAbs]
case inr.refine'_2
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
h : NeZero n
⊢ valMinAbs a * 2 < ↑n
case inr.refine'_2
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
h : NeZero n
⊢ -↑n < -valMinAbs a * 2
rw [neg_mul, neg_lt_neg_iff]
no goals
case inr.refine'_2
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
h : NeZero n
⊢ valMinAbs a * 2 < ↑n
exact a.valMinAbs_mem_Ioc.2.lt_of_ne (mt a.valMinAbs_mul_two_eq_iff.1 ha)
no goals
case inr.refine'_3
n : ℕ
a : ZMod n
ha : 2 * val a ≠ n
h : NeZero n
⊢ -valMinAbs a * 2 ≤ ↑n
linarith only [a.valMinAbs_mem_Ioc.1]