∀ {R : Type u_2} {M : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M)
  (motive : x ∈ {x | ∃ x_1, (∀ (n : M), (∃ a, a • x = n) → x_1 • n = 0) ∧ x_1 ≠ 0} → Prop)
  (x_1 : x ∈ {x | ∃ x_1, (∀ (n : M), (∃ a, a • x = n) → x_1 • n = 0) ∧ x_1 ≠ 0}),
  (∀ (a : R) (hax : ∀ (n : M), (∃ a, a • x = n) → a • n = 0) (ha : a ≠ 0), motive ⋯) → motive x_1