no goals
a b : Int
h : b ∣ a
⊢ div a b = a / b
if b0 : b = 0 then simp [b0]
else rw [Int.div_eq_iff_eq_mul_left b0 h, ← Int.ediv_eq_iff_eq_mul_left b0 h]
no goals
a b : Int
h : b ∣ a
b0 : b = 0
⊢ div a b = a / b
simp [b0]
no goals
a b : Int
h : b ∣ a
b0 : ¬b = 0
⊢ div a b = a / b
rw [Int.div_eq_iff_eq_mul_left b0 h, ← Int.ediv_eq_iff_eq_mul_left b0 h]