Right versus left derivative by increasing one-sided derivatives Condider a map $f:D\to\mathbb{R}$, $D$ open interval.
Let be $y,z\in D$, $y<z$. Suppose that $f$ has everywhere in $D$ both left and right derivative (this implies that $f$ is continuous), both increasing.
I want to show that
$$
f'(y^+)\le f'(z^-).
$$
I have found a way, but I'm not completely convinced that it is formally correct:
$$
f'(y^+)
=\lim_{\varepsilon\to 0^+}\frac{f(y+\varepsilon)-f(y)}{\varepsilon}
\overset{\forall\delta}{\le} 
  f'((z-\delta)^+)
= \lim_{\varepsilon\to 0^+}\frac{f(z-\delta+\varepsilon)-f(z-\delta)}{\varepsilon}
\overset{\varepsilon=\delta}{=} \lim_{\varepsilon\to 0^+}\frac{f(z)-f(z-\varepsilon)}{\varepsilon}
=f'(z^-)
$$
where $\delta>0$ and $y<z-\delta$.

Is there a way to formalise my proof?

 A: (I'll use the notation $f'_+$ and $f'_-$ for the right and left derivative.)
Unfortunately your proof does not work. This
$$
\lim_{\varepsilon\to 0^+}\frac{f(z-\delta+\varepsilon)-f(z-\delta)}{\varepsilon}
\overset{\varepsilon=\delta}{=} \lim_{\varepsilon\to 0^+}\frac{f(z)-f(z-\varepsilon)}{\varepsilon}
$$
makes no sense because $\delta$ is fixed and the limits are taken for $\varepsilon \to 0 $. Also it would imply that $f'_+(z-\delta) = f'_-(z)$ for $0 < \delta < z-y$, which is true only if $f$ is linear between $y$ and $z$.

What we can show is that
$$ \tag{*}
 f'_+(y) \le \frac{f(z)-f(y)}{z-y} \le f'_-(z)
$$
for $y < z$, which implies the desired conclusion. (This is motivated by the fact that both an increasing right derivative and an increasing left derivative imply that $f$ is convex.)
The proof of $(*)$ mimics the proof of Rolle's theorem and the mean-value theorem. We consider the function
$$
 g(x) = f(x) - (x-y)\frac{f(z)-f(y)}{z-y}
$$
which is continuous and satisfies $g(y) = g(z)$. It follows that $g$ attains its maximum on the interval $[y, z]$ at some point $w \in [y, z)$. Then $g'_+(w) \le 0$ and it follows that
$$
f'_+(y) \le f'_+(w) = g'_+(w) + \frac{f(z)-f(y)}{z-y} \le \frac{f(z)-f(y)}{z-y} \, .
$$
This proves the left inequality in $(*)$, the proof of the right inequality works similarly.
A: We can prove the stronger statement  $$\lim_{x\to y^+}f'_-(x)=f'_+(y)$$
By the Monotone Convergence Theorem $\lim_{x\to y^+}f'_-(x)$ exists. Call that limit $A$.
Now, let $\epsilon>0$ be given and choose a value of $\delta>0$ such that both of these are true:
$$x\in(y,y+\delta] \implies f'_-(x)\in \left[A,A+\frac{\epsilon}2 \right]$$
and
$$\left|\frac{f(y+\delta)-f(y)}{\delta}-f'_+(y)\right|\le \frac{\epsilon}2$$
That is possible because of the definitions of the left hand derivative and the limit.
Similar to the answer from @MartinR, define the function $g(x)=f(x)-\frac{f(y+\delta)-f(y)}{\delta}(x-y)$ so that $g(y)=g(y+\delta)$ and both $g'_-(x)=f'_-(x)-\frac{f(y+\delta)-f(y)}{\delta}$ and $g'_+(x)=f'_+(x)-\frac{f(y+\delta)-f(y)}{\delta}$ are increasing.
Claim 1. $g'_+(y) \le 0$
This follows because if it were not true, then $g'_+(x)$ would have to be positive for all $x\in  (y,y+\delta)$. That would imply $g$ is increasing (proof here) in that interval and it would be impossible for $g(y+\delta)$ to equal $g(y)$.
Claim 2. $g'_-(y+\delta) \ge 0$
Same argument as Claim 1. If it were not true, then $g'_-$ would have to be negative in the whole interval which would make it impossible for the function to have the same value at both ends of the interval.
Now,
$$g'_-(y+\delta)\ge0$$
$$f'_-(y+\delta)-\frac{f(y+\delta)-f(y)}{\delta}\ge0$$
$$f'_-(y+\delta) \ge \frac{f(y+\delta)-f(y)}{\delta} \ge f'_+(y)-\frac{\epsilon}2$$
We also know that $f'_-(y+\delta)\in \left[A,A+\frac{\epsilon}2 \right]$
Thus,
$$A \ge f'_-(y+\delta)-\frac{\epsilon}2 \ge f'_+(y)-\epsilon \label{eq1}\tag{1}$$
On the other hand,
$$g'_-(y)\le0$$
$$f'_-(y)-\frac{f(y+\delta)-f(y)}{\delta}\le0$$
$$f'_-(y) \le \frac{f(y+\delta)-f(y)}{\delta} \le f'_+(y)+\frac{\epsilon}2$$
So,
$$A \le f'_-(y+\delta) \le f'_+(y)+\frac{\epsilon}2 \label{eq2}\tag{2}$$
Combining the two inequalities (1) and (2), since $\epsilon$ was arbitrary, we have $A=f'_+(y)$.
To answer the original question, if $z>y$ then by the monotonicity assumption $f'_-(z)>\lim_{x\to y^+}f'_-(x)=f'_+(y)$
