Theorem: gaussInt.norm_conj (LeanCourse/MIL/C06_Structures/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean)

State before:
x : gaussInt
⊢ norm (conj x) = norm x
Tactic:
simp [norm]
State after:
no goals