{K : Type u_2} →
  [toSemiring : Semiring K] →
    [toInv : Inv K] →
      [toDiv : Div K] →
        autoParam (∀ (a b : K), a / b = a * b⁻¹) DivInvMonoid.div_eq_mul_inv._autoParam →
          (zpow : ℤ → K → K) →
            autoParam (∀ (a : K), zpow 0 a = 1) DivInvMonoid.zpow_zero'._autoParam →
              autoParam (∀ (n : ℕ) (a : K), zpow (↑n.succ) a = zpow (↑n) a * a) DivInvMonoid.zpow_succ'._autoParam →
                autoParam (∀ (n : ℕ) (a : K), zpow (Int.negSucc n) a = (zpow (↑n.succ) a)⁻¹)
                    DivInvMonoid.zpow_neg'._autoParam →
                  [toNontrivial : Nontrivial K] →
                    0⁻¹ = 0 →
                      (∀ (a : K), a ≠ 0 → a * a⁻¹ = 1) →
                        [toNNRatCast : NNRatCast K] →
                          autoParam (∀ (q : ℚ≥0), ↑q = ↑q.num / ↑q.den) DivisionSemiring.nnratCast_def._autoParam →
                            (nnqsmul : ℚ≥0 → K → K) →
                              autoParam (∀ (q : ℚ≥0) (a : K), nnqsmul q a = ↑q * a)
                                  DivisionSemiring.nnqsmul_def._autoParam →
                                DivisionSemiring K