Theorem: Associated'.norm_eq (FltRegular/FltThree/Edwards.lean)

State before:
x y : ℤ√(-3)
h : Associated' x y
⊢ x.norm = y.norm
Tactic:
cases' h with h h <;> simp only [Zsqrtd.norm_eq_of_associated (by norm_num) h, Zsqrtd.norm_conj]
State after:
no goals

State before:
x y : ℤ√(-3)
h : Associated x (star y)
⊢ -3 ≤ 0
Tactic:
norm_num
State after:
no goals