k n : ℕ
h✝ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝)
⊢ ↑(if val x ≤ namedPattern k (n + 1) h✝ / 2 then ↑(val x) else ↑(val x) - ↑(namedPattern k (n + 1) h✝)) = x
k n : ℕ
h✝ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝)
⊢ ↑(valMinAbs x) = x
rw [valMinAbs_def_pos]
case inl
k n : ℕ
h✝¹ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝¹)
h✝ : val x ≤ namedPattern k (n + 1) h✝¹ / 2
⊢ ↑↑(val x) = x

case inr
k n : ℕ
h✝¹ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝¹)
h✝ : ¬val x ≤ namedPattern k (n + 1) h✝¹ / 2
⊢ ↑(↑(val x) - ↑(namedPattern k (n + 1) h✝¹)) = x
k n : ℕ
h✝ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝)
⊢ ↑(if val x ≤ namedPattern k (n + 1) h✝ / 2 then ↑(val x) else ↑(val x) - ↑(namedPattern k (n + 1) h✝)) = x
split_ifs
no goals
case inl
k n : ℕ
h✝¹ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝¹)
h✝ : val x ≤ namedPattern k (n + 1) h✝¹ / 2
⊢ ↑↑(val x) = x
rw [Int.cast_ofNat, nat_cast_zmod_val]
no goals
case inr
k n : ℕ
h✝¹ : k = n + 1
x : ZMod (namedPattern k (n + 1) h✝¹)
h✝ : ¬val x ≤ namedPattern k (n + 1) h✝¹ / 2
⊢ ↑(↑(val x) - ↑(namedPattern k (n + 1) h✝¹)) = x
rw [Int.cast_sub, Int.cast_ofNat, nat_cast_zmod_val, Int.cast_ofNat, nat_cast_self, sub_zero]