Theorem: Zsqrt3.norm_natAbs (FltRegular/FltThree/Edwards.lean)

State before:
a : ℤ√(-3)
⊢ ↑a.norm.natAbs = a.norm
Tactic:
rw [Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) a)]
State after:
no goals

State before:
a : ℤ√(-3)
⊢ -3 ≤ 0
Tactic:
norm_num
State after:
no goals