Define $EXPTIME = TIME(2^n)$ and $NEXPTIME=NTIME(2^n)$.Use the function $pad$ to prove that: $$NEXPTIME \neq EXPTIME \implies P \neq NP$$$$pad(A, f(|s|)) = \{ s\#^{\max(0, f(|s|)-|s|)} \ |\ s \in A \}$$Solution:We shall prove the contrapositive. Suppose that $P=NP$. Then, consider any language $L \in NEXPTIME$, and let $c$ be a positive integer such that $L \in NTIME(2^{n^c})$. Then, it is easy to see that $pad(L,2^{n^c}) \in NP$. By assumption, $P= NP$, so $pad(L,2^{n^c}) \in P$ and therefore $L \in TIME(2^{n^c}) \subseteq EXPTIME$. It follows that $EXPTIME=NEXPTIME$.I agree that it is easy to intuitively see it, but I don't know how to prove it formally? We can words something  like $aba\#\#\#\#\#\#$. So, it seems that it is possible to measure length of $w = aba$ in $|w|^2$ time, yeah?
Proof of $NEXPTIME \neq EXPTIME \implies P \neq NP$
complexity theory