∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : BinomialRing R] [inst_2 : Semiring A] [inst_3 : SMul R A]
  (r : R) (n : ℕ), (PowerSeries.coeff n) (PowerSeries.binomialSeries A r) = Ring.choose r n • 1