Depth at a prime is bounded by local support dimension

Put $A=R_{\mathfrak{p}}$. Let $N$ be a nonzero finite $A$-module and let $x$ in the maximal ideal be $N$-regular. Then $\mathrm{Supp}(N\mathrm{/}xN)=\mathrm{Supp}(N)\cap V(x)$ by localization and Nakayama. A minimal prime $\mathfrak{q}$ of $\mathrm{Supp}(N)$ cannot contain $x$: otherwise $N_{\mathfrak{q}}$ has support only at the maximal ideal of $A_{\mathfrak{q}}$, so a power of $x$ annihilates it, contradicting injectivity on that nonzero localization. Any prime chain in $\mathrm{Supp}(N\mathrm{/}xN)$ can therefore be extended downward by a strict inclusion from a minimal prime of $\mathrm{Supp}(N)$. Hence $\dim \mathrm{Supp}(N\mathrm{/}xN)\le \dim \mathrm{Supp}(N)-1$. Conversely, lift a parameter tuple for $N\mathrm{/}xN$ and prepend $x$. Its quotient has finite length, so thm-dimension-and-parameters-for-modules gives $\dim \mathrm{Supp}(N)\le 1+\dim \mathrm{Supp}(N\mathrm{/}xN)$. Thus the dimension drops exactly one, without any catenarity assumption. All dimensions are finite by that module-dimension theorem (ultimately the local height bound).

Starting with $M_{\mathfrak{p}}$, every regular sequence of length $r$ has nonzero successive quotients by def-regular-sequence-on-a-module. Applying step 1.1 successively gives $r\le \dim {\mathrm{Supp}}_A(M_{\mathfrak{p}})$. Extending a sequence while possible must therefore stop, so a maximal sequence exists. The maximal ideal is the Jacobson radical, and Nakayama gives $\mathfrak{p}A{M}_{\mathfrak{p}}\mathrm{\ne }{M}_{\mathfrak{p}}$. Thus thm-depth-equals-maximal-regular-sequence-length identifies its length with depth, proving the asserted inequality. This also handles dimension zero, when the maximal sequence is empty.