apply Int.ediv_lt_of_lt_mul
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 }
H2 : (x % y).norm * y.norm ≤ y.norm / 2 * y.norm
⊢ y.norm / 2 < y.norm
case H
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 }
H2 : (x % y).norm * y.norm ≤ y.norm / 2 * y.norm
⊢ 0 < 2

case H'
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 }
H2 : (x % y).norm * y.norm ≤ y.norm / 2 * y.norm
⊢ y.norm < y.norm * 2