case zero
n a✝ : ℕ
a b : ZMod Nat.zero
⊢ Int.natAbs (valMinAbs (a + b)) ≤ Int.natAbs (valMinAbs a + valMinAbs b)

case succ
n✝ a✝ n : ℕ
a b : ZMod (Nat.succ n)
⊢ Int.natAbs (valMinAbs (a + b)) ≤ Int.natAbs (valMinAbs a + valMinAbs b)
n✝ a✝ n : ℕ
a b : ZMod n
⊢ Int.natAbs (valMinAbs (a + b)) ≤ Int.natAbs (valMinAbs a + valMinAbs b)
cases' n with n
case succ.he
n✝ a✝ n : ℕ
a b : ZMod (Nat.succ n)
⊢ ↑(valMinAbs (a + b)) = ↑(valMinAbs a + valMinAbs b)

case succ.hl
n✝ a✝ n : ℕ
a b : ZMod (Nat.succ n)
⊢ Int.natAbs (valMinAbs (a + b)) ≤ Nat.succ n / 2
case succ
n✝ a✝ n : ℕ
a b : ZMod (Nat.succ n)
⊢ Int.natAbs (valMinAbs (a + b)) ≤ Int.natAbs (valMinAbs a + valMinAbs b)
apply natAbs_min_of_le_div_two n.succ
no goals
case zero
n a✝ : ℕ
a b : ZMod Nat.zero
⊢ Int.natAbs (valMinAbs (a + b)) ≤ Int.natAbs (valMinAbs a + valMinAbs b)
rfl
no goals
case succ.he
n✝ a✝ n : ℕ
a b : ZMod (Nat.succ n)
⊢ ↑(valMinAbs (a + b)) = ↑(valMinAbs a + valMinAbs b)
simp_rw [Int.cast_add, coe_valMinAbs]
no goals
case succ.hl
n✝ a✝ n : ℕ
a b : ZMod (Nat.succ n)
⊢ Int.natAbs (valMinAbs (a + b)) ≤ Nat.succ n / 2
apply natAbs_valMinAbs_le