no goals
a : ℤ
⊢ (↑a)⁻¹.den = if a = 0 then 1 else Int.natAbs a
induction a using Int.induction_on <;>
  simp [← Int.negSucc_coe', Int.negSucc_coe, -neg_add_rev, Rat.inv_neg, Int.ofNat_add_one_out,
    -Nat.cast_succ, inv_coe_nat_den_of_pos, -Int.cast_negSucc, ofInt_eq_cast]