∀ {R : Type u} [inst : CommRing R] [IsPrincipalIdealRing R] {M : Type v} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [IsDomain R] {p : R},
  Irreducible p →
    ∀ (hM : Module.IsTorsion' M ↥(Submonoid.powers p)) [dec : (x : M) → Decidable (x = 0)] (x : M),
      Ideal.torsionOf R M x = Ideal.span {p ^ Submodule.pOrder hM x}