{G₀ : Type u} →
  (mul : G₀ → G₀ → G₀) →
    (∀ (a b c : G₀), a * b * c = a * (b * c)) →
      (one : G₀) →
        (∀ (a : G₀), 1 * a = a) →
          (∀ (a : G₀), a * 1 = a) →
            (npow : ℕ → G₀ → G₀) →
              autoParam (∀ (x : G₀), npow 0 x = 1) Monoid.npow_zero._autoParam →
                autoParam (∀ (n : ℕ) (x : G₀), npow (n + 1) x = npow n x * x) Monoid.npow_succ._autoParam →
                  (zero : G₀) →
                    (∀ (a : G₀), 0 * a = 0) →
                      (∀ (a : G₀), a * 0 = 0) →
                        (inv : G₀ → G₀) →
                          (div : G₀ → G₀ → G₀) →
                            autoParam (∀ (a b : G₀), a / b = a * inv b) DivInvMonoid.div_eq_mul_inv._autoParam →
                              (zpow : ℤ → G₀ → G₀) →
                                autoParam (∀ (a : G₀), zpow 0 a = 1) DivInvMonoid.zpow_zero'._autoParam →
                                  autoParam (∀ (n : ℕ) (a : G₀), zpow (↑n.succ) a = zpow (↑n) a * a)
                                      DivInvMonoid.zpow_succ'._autoParam →
                                    autoParam (∀ (n : ℕ) (a : G₀), zpow (Int.negSucc n) a = inv (zpow (↑n.succ) a))
                                        DivInvMonoid.zpow_neg'._autoParam →
                                      (∃ x y, x ≠ y) →
                                        inv 0 = 0 → (∀ (a : G₀), a ≠ 0 → a * inv a = 1) → GroupWithZero G₀