simp only [mul_zero] at h₀
case intro.inl
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * 0
hc : c = 0
x✝ : ¬|i| ≤ |j|
⊢ False
case intro.inl
i j : ℤ
gj : 0 ≠ j
c : ℤ
hc : c = 0
x✝ : ¬|i| ≤ |j|
h₀ : j = 0
⊢ False