∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : DecidableEq σ] (n : σ →₀ ℕ) (a : R) (φ : MvPowerSeries σ R),
  (MvPowerSeries.coeff n) (MvPowerSeries.inv.aux a φ) =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ Finset.antidiagonal n,
          if x.2 < n then (MvPowerSeries.coeff x.1) φ * (MvPowerSeries.coeff x.2) (MvPowerSeries.inv.aux a φ) else 0