gcongr <;> apply Int.abs_mod'_le _ _ norm_y_pos
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.re * y.re + x.im * y.im).mod' y.norm| ^ 2 + |(-(x.re * y.im) + x.im * y.re).mod' y.norm| ^ 2 ≤
    (y.norm / 2) ^ 2 + (y.norm / 2) ^ 2
no goals