have H1 : x % y * conj y = ⟨Int.mod' (x * conj y).re (norm y), Int.mod' (x * conj y).im (norm y)⟩
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
⊢ (x % y).norm < y.norm
case H1
x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
⊢ x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }

x y : GaussInt
hy : y ≠ 0
norm_y_pos : 0 < y.norm
H1 : x % y * y.conj = { re := (x * y.conj).re.mod' y.norm, im := (x * y.conj).im.mod' y.norm }
⊢ (x % y).norm < y.norm