case inl
h : 0 ≤ 0
⊢ ↑normalize 0 = -0

case inr
z : ℤ
h✝ : z ≤ 0
h : z < 0
⊢ ↑normalize z = -z
z : ℤ
h : z ≤ 0
⊢ ↑normalize z = -z
obtain rfl | h := h.eq_or_lt
no goals
case inl
h : 0 ≤ 0
⊢ ↑normalize 0 = -0
simp
no goals
case inr
z : ℤ
h✝ : z ≤ 0
h : z < 0
⊢ ↑normalize z = -z
rw [normalize_apply, normUnit_eq, if_neg (not_le_of_gt h), Units.val_neg, Units.val_one,
  mul_neg_one]