Theorem: Associated'.norm_eq (Flt/Edwards.lean)

State before:
x y : ℤ√(-3)
h : Associated' x y
⊢ Zsqrtd.norm x = Zsqrtd.norm y
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