case inl

⊢ ‖↑(0 / 2)‖ = abs 0 / 2

case inr
p : ℝ
hp : p ≠ 0
⊢ ‖↑(p / 2)‖ = abs p / 2
p : ℝ
⊢ ‖↑(p / 2)‖ = abs p / 2
rcases eq_or_ne p 0 with (rfl | hp)
no goals
case inr
p : ℝ
hp : p ≠ 0
⊢ ‖↑(p / 2)‖ = abs p / 2
rw [norm_eq, ← mul_div_assoc, inv_mul_cancel hp, one_div, round_two_inv, Int.cast_one,
  one_mul, (by linarith : p / 2 - p = -(p / 2)), abs_neg, abs_div, abs_two]
no goals
case inl

⊢ ‖↑(0 / 2)‖ = abs 0 / 2
simp
no goals
p : ℝ
hp : p ≠ 0
⊢ p / 2 - p = -(p / 2)
linarith