a b c : Int
H : a ∣ c
h : a ∣ b + c
this : a ∣ b + c - c
⊢ a ∣ b
a b c : Int
H : a ∣ c
h : a ∣ b + c
⊢ a ∣ b
have := Int.dvd_sub h H
no goals
a b c : Int
H : a ∣ c
h : a ∣ b + c
this : a ∣ b + c - c
⊢ a ∣ b
rwa [Int.add_sub_cancel] at this