Theorem: GaussInt.norm_pos (MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean)

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

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