∀ {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst_1 : AddCommMonoid M] [inst_2 : DistribMulAction R M] {p p_1 : R}
  (e_p : p = p_1) (hM : Module.IsTorsion' M ↥(Submonoid.powers p)) (x x_1 : M),
  x = x_1 →
    ∀ {inst_3 : (n : ℕ) → Decidable (p ^ n • x = 0)} [inst_4 : (n : ℕ) → Decidable (p_1 ^ n • x_1 = 0)],
      Submodule.pOrder hM x = Submodule.pOrder ⋯ x_1