no goals
a b : ℤ
hb0 : 0 < b
h : Nat.coprime (Int.natAbs a) (Int.natAbs b)
⊢ ↑(↑a / ↑b).den = b
rw [←Int.natAbs_of_nonneg hb0.le, ← Rat.divInt_eq_div,
  ←mk_eq_divInt _ _ (Int.natAbs_ne_zero.mpr hb0.ne') h]