∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (A : VertexOperator R V) (n : ℤ) (x : V),
  -n - 1 < ((HahnModule.of R).symm (A x)).order → (VertexOperator.ncoeff A n) x = 0