no goals
a b : Int
⊢ a ∣ -b ↔ a ∣ b
constructor <;> exact fun ⟨k, e⟩ =>
  ⟨-k, by simp [← e, Int.neg_mul, Int.mul_neg, Int.neg_neg]⟩
no goals
a b : Int
x✝ : a ∣ b
k : Int
e : b = a * k
⊢ -b = a * -k
simp [← e, Int.neg_mul, Int.mul_neg, Int.neg_neg]