Show that $\frac{1}{\cosh(x)} + \log\left(\frac{\cosh(x)}{1+\cosh(x)}\right) \ge 0$ I want to show that the following is true:

$$\frac{1}{\cosh(x)} + \log(\frac{\cosh(x)}{1+\cosh(x)}) \ge 0$$

Below is how I approached it, but I did not end up with an acceptable answer.
\begin{align}
\frac{1}{\cosh(x)} + \log\left(\frac{\cosh(x)}{1+\cosh(x)}\right)
& = \log\left(e^{\frac{1}{\cosh(x)}}\right) + \log\left(\frac{\cosh(x)}{1+\cosh(x)}\right) \\
& = \log\left(\frac{e^{\frac{1}{\cosh(x)}} \cdot \cosh(x)}{1+\cosh(x)}\right).
\end{align} 
I don't know where to go from here so that I can show that this non-negative.
 A: A slicker approach is to rewrite the identity as $$s:=\operatorname{sech}x\ge-\ln\frac{\cosh x}{1+\cosh x}=\ln\frac{1+\cosh x}{\cosh x}=\ln (1+s),$$which is trivial from the famous inequality $\exp y\ge 1+y$ with $y:=\ln (1+s)$.
A: Consider the map$$\begin{array}{rccc}f\colon&[1,\infty)&\longrightarrow&\mathbb R\\&x&\mapsto&\frac1x+\log\left(\frac x{x+1}\right).\end{array}$$It is clear that $\lim_{x\to\infty}f(x)=0.$ On the other hand,$$(\forall x\in[1,\infty)):f'(x)=-\frac1{x^2+x^3}$$and therefore $f$ is strictly decreasing. So, $(\forall x\in[1,\infty)):f(x)>0$. But your function is $f\bigl(\cosh(x)\bigr)$.
A: Let $\cosh(x)=t$, then $t \ge 1$.  In this case, the inequality becomes
$$
\frac{1}{t}+\ln\left(\frac{t}{1+t}\right)\ge 0.
$$
Three observations:


*

*When $t=1$, we get $1+\ln\frac{1}{2}\geq 0$.  This is true since $1+\ln\frac{1}{e}=0$ and $\frac{1}{2}\geq\frac{1}{e}$.

*The derivative of the LHS is 
$$
-\frac{1}{t^2}+\frac{1}{t(t+1)}\le 0.
$$
Therefore, the LHS is decreasing.

*The limit as $t$ approaches infinity is
$$
\lim_{t\to \infty}\frac{1}{t} + \ln\left(\frac{t}{1+t}\right)
=0.
$$
Putting these together, we get that the LHS is greater than $0$ when $t=1$ and decreases to $0$ as $t$ approaches infinity.  Therefore, the LHS is positive for all $t$.
