Theorem: gaussInt.natAbs_norm_mod_lt (LeanCourse/MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean)

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

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

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