∀ {σ : Type u_1} {R : Type u_3} [Finite σ] [inst : CommRing R] (p : ℕ),
  p ≠ 0 →
    ∀ {n m : σ →₀ ℕ},
      n ≤ m →
        ∀ [inst_1 : DecidableEq σ] (f : MvPowerSeries σ R),
          (MvPolynomial.expand p) ((MvPowerSeries.trunc' R n) f) =
            (MvPowerSeries.trunc' R (p • n)) ↑((MvPolynomial.expand p) ((MvPowerSeries.trunc' R m) f))