regular local quotient by parameter is regular

Given: The objects and hypotheses in the statement. We work with the Axiom of Choice; cited dependent-choice and resolution-existence hypotheses are retained.

regular system of parameters equivalent basis: Let $(R,\mathfrak{m},k)$ be a nonzero Noetherian local ring of dimension $d$, and let $\mathbf{x}=(x_1,\dots ,x_d)\in {\mathfrak{m}}^d$. Then $\mathbf{x}$ is a regular system of parameters if and only if its classes form a $k$-basis of $\mathfrak{m}\mathrm{/}{\mathfrak{m}}^2$. In particular every lift of a cotangent basis in a regular local ring generates $\mathfrak{m}$ and is a system of parameters.

dimension at most embedding dimension: Every nonzero commutative Noetherian local ring $R$ satisfies $\dim R\le \mathrm{edim}R<\mathrm{\infty }$.

Local dimension is the minimal number of generators of an ideal with maximal radical: Let $(R,\mathfrak{m})$ be a finite-dimensional Noetherian local ring of dimension $d<\mathrm{\infty }$. Then $d$ is the least integer $n$ for which there exists an $n$-generated ideal $J\subseteq R$ with $\sqrt{J}=\mathfrak{m}$.