no goals
a b c : Int
H : c ∣ b
h : c = 0
⊢ (a + b) / c = a / c + b / c
simp [h]
a b c : Int
H : c ∣ b
h : ¬c = 0
k : Int
hk : b = c * k
⊢ (a + b) / c = a / c + b / c
a b c : Int
H : c ∣ b
h : ¬c = 0
⊢ (a + b) / c = a / c + b / c
let ⟨k, hk⟩ := H
no goals
a b c : Int
H : c ∣ b
h : ¬c = 0
k : Int
hk : b = c * k
⊢ (a + b) / c = a / c + b / c
rw [hk, Int.mul_comm c k, Int.add_mul_ediv_right _ _ h,
  ← Int.zero_add (k * c), Int.add_mul_ediv_right _ _ h, Int.zero_ediv, Int.zero_add]