simp only [hcube, Zsqrtd.norm_def, hA]
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
⊢ r ^ 3 = Zsqrtd.norm A
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
⊢ a ^ 2 + 3 * b ^ 2 = a * a - -3 * b * b