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

State before:
x y : GaussInt
hy : y ≠ 0
⊢ (x % y).norm.natAbs < y.norm.natAbs
Tactic:
apply Int.ofNat_lt.1
State after:
x y : GaussInt
hy : y ≠ 0
⊢ ↑(x % y).norm.natAbs < ↑y.norm.natAbs

State before:
x y : GaussInt
hy : y ≠ 0
⊢ ↑(x % y).norm.natAbs < ↑y.norm.natAbs
Tactic:
simp only [Int.coe_natAbs, abs_of_nonneg, norm_nonneg]
State after:
x y : GaussInt
hy : y ≠ 0
⊢ (x % y).norm < y.norm

State before:
x y : GaussInt
hy : y ≠ 0
⊢ (x % y).norm < y.norm
Tactic:
apply norm_mod_lt x hy
State after:
no goals