case zero
a : ℕ
ha : Nat.zero / 2 < a
ha' : a < Nat.zero
⊢ valMinAbs ↑a = ↑a - ↑Nat.zero

case succ
a n✝ : ℕ
ha : Nat.succ n✝ / 2 < a
ha' : a < Nat.succ n✝
⊢ valMinAbs ↑a = ↑a - ↑(Nat.succ n✝)
n a : ℕ
ha : n / 2 < a
ha' : a < n
⊢ valMinAbs ↑a = ↑a - ↑n
cases n
no goals
case zero
a : ℕ
ha : Nat.zero / 2 < a
ha' : a < Nat.zero
⊢ valMinAbs ↑a = ↑a - ↑Nat.zero
cases not_lt_bot ha'
no goals
case succ
a n✝ : ℕ
ha : Nat.succ n✝ / 2 < a
ha' : a < Nat.succ n✝
⊢ valMinAbs ↑a = ↑a - ↑(Nat.succ n✝)
simp [valMinAbs_def_pos, val_nat_cast, Nat.mod_eq_of_lt ha', ha.not_le]