calc
  |i| ≤ (|i|)*|c| := by
      exact le_mul_of_le_of_one_le' rfl.ge (Int.one_le_abs h) (abs_nonneg c) (abs_nonneg i)
    _ = |i*c| := Eq.symm (abs_mul i c)
    _ = |j| := by rw [Eq.symm h₀]
case intro.inr
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
h : ¬c = 0
⊢ |i| ≤ |j|
no goals