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

State before:
x : gaussInt
⊢ 0 < norm x ↔ x ≠ 0
Tactic:
rw [lt_iff_le_and_ne, ne_comm, Ne, norm_eq_zero]
State after:
x : gaussInt
⊢ 0 ≤ norm x ∧ ¬x = 0 ↔ x ≠ 0

State before:
x : gaussInt
⊢ 0 ≤ norm x ∧ ¬x = 0 ↔ x ≠ 0
Tactic:
simp [norm_nonneg]
State after:
no goals