Why can't this identity hold problem be solved?
Resolve[ForAll[n, n \[Element] PositiveIntegers, \[Lambda] <= -7 n + 2 n^2]]
It is disappointing, because Mathematica can do this easily:
In[15]:= Minimize[{-7 n + 2 n^2, n > 0}, n \[Element] Integers] Out[15]= {-6, {n -> 2}}
