no goals
a b : Int
H✝ : b ≠ 0
a✝ b✝ : Nat
H : ↑b✝ ≠ 0
⊢ div (↑a✝ * ↑b✝) ↑b✝ = ↑a✝
rw [← ofNat_mul, ← ofNat_div,
  Nat.mul_div_cancel _ <| Nat.pos_of_ne_zero <| Int.ofNat_ne_zero.1 H]
no goals
a✝ b✝ : Int
this : ∀ {a b : Nat}, ↑b ≠ 0 → div (↑a * ↑b) ↑b = ↑a
a b : Nat
H : -↑b ≠ 0
⊢ div (↑a * -↑b) (-↑b) = ↑a
rw [Int.mul_neg, Int.neg_div, Int.div_neg, Int.neg_neg,
  this (Int.neg_ne_zero.1 H)]
no goals
a✝ b✝ : Int
this : ∀ {a b : Nat}, ↑b ≠ 0 → div (↑a * ↑b) ↑b = ↑a
a b : Nat
H : ↑b ≠ 0
⊢ div (-↑a * ↑b) ↑b = -↑a
rw [Int.neg_mul, Int.neg_div, this H]
no goals
a✝ b✝ : Int
this : ∀ {a b : Nat}, ↑b ≠ 0 → div (↑a * ↑b) ↑b = ↑a
a b : Nat
H : -↑b ≠ 0
⊢ div (-↑a * -↑b) (-↑b) = -↑a
rw [Int.neg_mul_neg, Int.div_neg, this (Int.neg_ne_zero.1 H)]