∀ (A : Type u_1) [inst : AddGroup A] [inst_1 : DivisibleBy A ℕ],
  AddGroup.divisibleByIntOfDivisibleByNat A =
    {
      div := fun a z =>
        match z with
        | Int.ofNat n => DivisibleBy.div a n
        | Int.negSucc n => -DivisibleBy.div a (n + 1),
      div_zero := ⋯, div_cancel := ⋯ }