no goals
a b : Int
H : b ≠ 0
b0 : 0 ≤ b
⊢ fdiv (a * b) b = a
rw [fdiv_eq_ediv _ b0, mul_ediv_cancel _ H]
no goals
a b x✝¹ : Int
x✝ : x✝¹ < 0
H : x✝¹ ≠ 0
b0 : ¬0 ≤ x✝¹
⊢ fdiv (0 * x✝¹) x✝¹ = 0
simp [Int.zero_mul]