calc
  norm (x % y) * norm y = norm (x % y * conj y) := by simp only [norm_mul, norm_conj]
  _ = |Int.mod' (x.re * y.re + x.im * y.im) (norm y)| ^ 2
      + |Int.mod' (-(x.re * y.im) + x.im * y.re) (norm y)| ^ 2 := by simp [H1, norm, sq_abs]
  _ ≤ (y.norm / 2) ^ 2 + (y.norm / 2) ^ 2 := by gcongr <;> apply Int.abs_mod'_le _ _ norm_y_pos
  _ = norm y / 2 * (norm y / 2 * 2) := by ring
  _ ≤ norm y / 2 * norm y := by gcongr; apply Int.ediv_mul_le; norm_num
case H2
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 ≤ y.norm / 2 * y.norm
no goals