∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α] {n : ℕ},
  AddAction.IsMultiplyPreprimitive M α n → ∀ {m : ℕ}, m ≤ n → ↑n ≤ ENat.card α → AddAction.IsMultiplyPreprimitive M α m