Is there any automated (i.e., some algorithm) to prove that a certain algebraic expression is always non-negative in some range ? If so, is there any implementation you would suggest? My concrete problem is that I want to prove that for $f \in [0,1], 1 \leq a \leq L-2$ the following is true:

$$2^{(-a - L)} f^{-a} (1 + f)^{(-1 - a)} \left\{2^{(1 + a)} f^a (1 + f)^L (1 + 2 f) \left(-(1 + f)^{(1 + a)} + 2^a (1 + f^{(1 + a)})\right)\right.$$
$$ + 2^L (1 + f)^a \left[-2^a (1 + f) \left(-f^{(1 + 2 a)} + f^L + 3 f^{(a + L)} + 
3 f^{(1 + a + L)}\right) \right.$$
$$ \left.\left.+ (1 + f)^a \left((-3 + f) f^{(1 + a)} - a (-1 + f) (1 + 2 f) (f^a - f^L) + f^L (2 + 3 f (3 + f))\right)\right]\right\} >=0$$