a b c : Int
hcb : c ∣ b
⊢ a / c + -b / c = a / c + -(b / c)
a b c : Int
hcb : c ∣ b
⊢ (a - b) / c = a / c - b / c
rw [Int.sub_eq_add_neg, Int.sub_eq_add_neg, Int.add_ediv_of_dvd_right (Int.dvd_neg.2 hcb)]
case e_a
a b c : Int
hcb : c ∣ b
⊢ -b / c = -(b / c)
a b c : Int
hcb : c ∣ b
⊢ a / c + -b / c = a / c + -(b / c)
congr
no goals
case e_a
a b c : Int
hcb : c ∣ b
⊢ -b / c = -(b / c)
exact Int.neg_ediv_of_dvd hcb