In Sbiis Saibian's site I came across Polyates Lemma which states that
$$(b \uparrow^k m) \uparrow^k n\ <\ b\uparrow^k (m+n)$$
for all positive integers b,m,n,k with $b\ge 2$ and $k\ge 2$.
He promised to prove this in section $3.3$, but I could not find it there.
Of course, I thought of induction. But should I do it over $m$, over $n$ or a double induction ?
The base case is clear, but I did not manage the induction step.
I detailed a complete proof here: https://sites.google.com/site/largenumbers/home/appendix/c
-- Sbiis Saibian