case inl
a b : ℤ
H : b ∣ a
h : natAbs b = 0
⊢ natAbs (a / b) = natAbs a / natAbs b

case inr
a b : ℤ
H : b ∣ a
h : natAbs b > 0
⊢ natAbs (a / b) = natAbs a / natAbs b
a b : ℤ
H : b ∣ a
⊢ natAbs (a / b) = natAbs a / natAbs b
rcases Nat.eq_zero_or_pos (natAbs b) with (h | h)
case inl
a b : ℤ
H : b ∣ a
h : natAbs b = 0
⊢ natAbs (a / 0) = natAbs a / natAbs 0

case inr
a b : ℤ
H : b ∣ a
h : natAbs b > 0
⊢ natAbs (a / b) = natAbs a / natAbs b
case inl
a b : ℤ
H : b ∣ a
h : natAbs b = 0
⊢ natAbs (a / b) = natAbs a / natAbs b

case inr
a b : ℤ
H : b ∣ a
h : natAbs b > 0
⊢ natAbs (a / b) = natAbs a / natAbs b
rw [natAbs_eq_zero.1 h]
case inr
a b : ℤ
H : b ∣ a
h : natAbs b > 0
⊢ natAbs (a / b) = natAbs a / natAbs b
case inl
a b : ℤ
H : b ∣ a
h : natAbs b = 0
⊢ natAbs (a / 0) = natAbs a / natAbs 0

case inr
a b : ℤ
H : b ∣ a
h : natAbs b > 0
⊢ natAbs (a / b) = natAbs a / natAbs b
simp [Int.ediv_zero]
no goals
case inr
a b : ℤ
H : b ∣ a
h : natAbs b > 0
⊢ natAbs (a / b) = natAbs a / natAbs b
calc
  natAbs (a / b) = natAbs (a / b) * 1 := by rw [mul_one]
  _ = natAbs (a / b) * (natAbs b / natAbs b) := by rw [Nat.div_self h]
  _ = natAbs (a / b) * natAbs b / natAbs b := by rw [Nat.mul_div_assoc _ dvd_rfl]
  _ = natAbs (a / b * b) / natAbs b := by rw [natAbs_mul (a / b) b]
  _ = natAbs a / natAbs b := by rw [Int.ediv_mul_cancel H]
no goals
a b : ℤ
H : b ∣ a
h : natAbs b > 0
⊢ natAbs (a / b) = natAbs (a / b) * 1
rw [mul_one]
no goals
a b : ℤ
H : b ∣ a
h : natAbs b > 0
⊢ natAbs (a / b) * 1 = natAbs (a / b) * (natAbs b / natAbs b)
rw [Nat.div_self h]
no goals
a b : ℤ
H : b ∣ a
h : natAbs b > 0
⊢ natAbs (a / b) * (natAbs b / natAbs b) = natAbs (a / b) * natAbs b / natAbs b
rw [Nat.mul_div_assoc _ dvd_rfl]
no goals
a b : ℤ
H : b ∣ a
h : natAbs b > 0
⊢ natAbs (a / b) * natAbs b / natAbs b = natAbs (a / b * b) / natAbs b
rw [natAbs_mul (a / b) b]
no goals
a b : ℤ
H : b ∣ a
h : natAbs b > 0
⊢ natAbs (a / b * b) / natAbs b = natAbs a / natAbs b
rw [Int.ediv_mul_cancel H]