case zero
a : ℕ
ha : a ≤ Nat.zero / 2
⊢ valMinAbs ↑a = ↑a

case succ
a n✝ : ℕ
ha : a ≤ Nat.succ n✝ / 2
⊢ valMinAbs ↑a = ↑a
n a : ℕ
ha : a ≤ n / 2
⊢ valMinAbs ↑a = ↑a
cases n
no goals
case zero
a : ℕ
ha : a ≤ Nat.zero / 2
⊢ valMinAbs ↑a = ↑a
simp
no goals
case succ
a n✝ : ℕ
ha : a ≤ Nat.succ n✝ / 2
⊢ valMinAbs ↑a = ↑a
simp [valMinAbs_def_pos, val_nat_cast, Nat.mod_eq_of_lt (ha.trans_lt <| Nat.div_lt_self' _ 0),
  ha]