Is this proof about the derivability of $f$ at $0$ correct? I'm studing that if  $f : \mathbb{R} \rightarrow \mathbb{R} \phantom{2}$ is a function that  verifies :
$\exists\, K \in \mathbb{R^+}, \phantom{1}\forall\, x,y \in \mathbb{R}: \lvert f(y)-f(x) \rvert \le K\lvert \cos y - \cos x \rvert$
Then f is differentiable at $0$
We know that that $$  \lvert f(y)-f(x) \rvert \le K\lvert \cos y - \cos x \rvert;\forall\, x,y \in \mathbb{R},\\  \\ \implies \frac{| f(y)-f(x)|}{|y-x|}\le K\frac{\lvert \cos y - \cos x \rvert}{|y-x|}, \forall x\ne y $$
$\therefore \lim_{x\to 0} \frac{| f(0)-f(x)|}{|0-x|}\le K\cdot\lim_{x\to 0}\frac{\lvert \cos 0 - \cos x \rvert}{|0-x|}=K\cdot |\sin 0|=0$. This because $\cos $ is differentiable. 
So we have $\lim_{x\to 0} \frac{| f(0)-f(x)|}{|0-x|}=0$.
We know that $\lim_{x\to c}g(x)=0 \Leftrightarrow \lim_{x\to c}|g(x)|=0 $
and hence  $$f'(0)=\lim_{x\to 0}\frac{f(x)-f(0)}{x}=0$$
Is it correct to use the existence of $\lim_{x\to 0} \frac{| f(0)-f(x)|}{|0-x|}$ while we are proving it? And does $\lim_{x\to 0} \frac{| f(0)-f(x)|}{|0-x|}= \lvert \lim_{x\to 0}\frac{ f(0)-f(x)}{0-x}\rvert$?
 A: Another approach is to use squeeze theorem.
Just use the inequality $$0\leq\left|\frac{f(x)-f(0)}{x}\right|\leq K\cdot \frac {|\cos x - 1|}{|x|}$$ and apply squeeze theorem to get $f'(0)=0$.
A: There are a few issues. It is, as you suspect, not correct to use the existence of
$$\lim_{x \to 0} \frac{\lvert f(0) - f(x)\rvert}{\lvert 0-x\rvert}$$
while proving its existence.
This is remedied by using $\limsup$ there, which always exists (if $\pm\infty$ are allowed). Since the quotient is non-negative, we can then deduce that the limit exists and is $0$, for the $\limsup$ is $0$.
Then it is generally the case that the existence of
$$\lim_{x \to 0} \frac{f(0) - f(x)}{0-x}\tag{1}$$
implies the existence of
$$\lim_{x \to 0} \frac{\lvert f(0) - f(x)\rvert}{\lvert 0-x\rvert} \tag{2}$$
and we have the equality
$$\biggl\lvert \lim_{x \to 0} \frac{f(0) - f(x)}{0-x}\biggr\rvert = \lim_{x \to 0} \frac{\lvert f(0) - f(x)\rvert}{\lvert 0-x\rvert}\,,$$
but usually the existence of $(2)$ does not imply the existence of $(1)$ [consider the sequence $(-1)^n$ to see why]. However, here the limit $(2)$ is zero, and then the existence of $(2)$ implies that $(1)$ also exists and is zero.
