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