∀ (R : Type u_1) [inst : CommRing R] [NoZeroDivisors R] {m : ℕ},
  0 < m →
    (PowerSeries.mk fun n => ↑(Nat.Partition.restricted n fun x => ¬m ∣ x).card) =
      PowerSeries.mk fun n => ↑(Nat.Partition.countRestricted n m).card