a b c : Int
H : a ∣ b - -c
⊢ a ∣ b ↔ a ∣ c
a b c : Int
H : a ∣ b + c
⊢ a ∣ b ↔ a ∣ c
rw [← Int.sub_neg] at H
no goals
a b c : Int
H : a ∣ b - -c
⊢ a ∣ b ↔ a ∣ c
rw [Int.dvd_iff_dvd_of_dvd_sub H, Int.dvd_neg]