Q: Can't this inequality really not be solved with Reduce? Taking $\alpha$ as given, I am trying to understand/know under which restrictions on $n$, the following holds:
$$ 0 \leq n+\alpha W\left(-e^{\frac{-n}{\alpha}} \right) \leq 1.$$
i.e I want to solve for $n$ the following two inequalities: a) $0 \leq n+\alpha W\left(-e^{\frac{-n}{\alpha}} \right)$, and b) $n+\alpha W\left(-e^{\frac{-n}{\alpha}} \right) \leq 1$.
In addition, I know $\alpha >0$, that both $n$ and $\alpha$ are reals.

*

*I manage to get that a) is satisfied for $n\geq \alpha$,
using: Reduce[n+a*ProductLog[-E^(-n/a)]>=0, n, Reals] which returns (a<0&&n==a)||(a>0&&n≥a).

*However I struggle to find any solution for the inequality b). I have tried all of the following:

(* for convenience I first define the function *)
f[n_, a_] =n+a*ProductLog[-E^(-n/a)]

Reduce[f[n, a]<=1, n, Reals]
Reduce[f[n, a]<=1 && a>0, n, Reals]
Solve[f[n, a]<=1, n, Reals]
Solve[f[n, a]<=1 && a>0, n, Reals]

Which all return:
"This system cannot be solved with the methods available to Solve/Reduce."
Even though I specified the domain as suggested here.
Is the inequality in b) really not solvable for $n$? Could Anyone think of an alternative command or commands that would do the trick?
Thank you,
EDIT:
In my context, f[n_, a_]being strictly increasing in n, and also because I know that (due to the domain of the Lambert W function) we must have n ≥ a (on the graph of f[n, a]below, we see clearly that it is not defined otherwise), even the solution for the equality to 1 would suffice me.
Manipulate[Plot[f[n, a], {n, -1, 10}], {a, 0, 5, 0.05, Appearance -> "Labeled"}]



A: We can change variable.
f[n_, a_] = n + a*ProductLog[-E^(-n/a)];
f[n, a] <= 1 /. n -> t*a // Simplify


a (t + ProductLog[-E^-t]) <= 1

so for a>0 we just need to solve
t + ProductLog[-E^-t]<=1/a
Since
FunctionRange[D[t + ProductLog[-E^-t], t], t, y]


y > 1

so t + ProductLog[-E^-t] is increasing and we find its inverse.
InverseFunction[Function[t, t + ProductLog[-E^-t]]][1/a]


t<=1/a + E^(-1/a)


n/a<=1/a + E^(-1/a)


n<=1+a* E^(-1/a)

Edit
For a fixed a>0,both
f[n_, a_] = n + a*ProductLog[-E^(-n/a)];
Solve[f[n, a] == c, n]
InverseFunction[Function[n, f[n, a]]][c, a]

get

E^(-(c/a)) (a + c E^(c/a)

means that f[n,a]<=c is solvatable.
