no goals
b c : Int
⊢ -(b * c) / b = -(b * c / b)
if bz : b = 0 then simp [bz] else
rw [Int.neg_mul_eq_mul_neg, Int.mul_ediv_cancel_left _ bz, Int.mul_ediv_cancel_left _ bz]
no goals
b c : Int
bz : b = 0
⊢ -(b * c) / b = -(b * c / b)
simp [bz]
no goals
b c : Int
bz : ¬b = 0
⊢ -(b * c) / b = -(b * c / b)
rw [Int.neg_mul_eq_mul_neg, Int.mul_ediv_cancel_left _ bz, Int.mul_ediv_cancel_left _ bz]