Constructive Krull dimension (singular sequence in localization) In this question a constructive approach to Krull dimension is mentioned following this short note.
Since the paper is very short and probably well known, I am not copying its contents. I hope this is okay.
I am struggling with equation $(2)$ in Corollary 2 and the sentence preceding it. Namely, I don't understand why equation $(2)$ is equivalent to every length $\ell-1$ sequence in the localization $R[S^-1]$ being singular. I tried just opening the condition with fractions, but I get bogged down with large expressions and also don't see why the statement should be equivalent.
How to prove the sentence containing equation $(2)$?
 A: Corollary (2) of the paper states:

Let $R$ be a commutative ring and $l$ be a nonnegative integer.  The Krull dimension of $R$ is at most $l$ if and only if for any given $x_0, \ldots, x_l$ there exist $a_0,\ldots, a_l$ in $R$ and $m_0,\ldots,m_l$ in $\mathbb{N}$ such that $$x_0^{m_0}(\cdots(x_l^{m_l}(1+a_lx_l)+\cdots) +a_0x_0 ) = 0$$

Coquand and Lombardi proceed inductively, first establishing the base case for any $0$-dimensional ring from Theorem 1 of the paper (easy to do directly also).  To attack the inductive step, the key is reinterpreting the inductive hypothesis for localizations of a fixed ring $R$, in particular boundary rings of its elements (as defined in the paper).  

Let $R$ be a ring, $S$ a multiplicative set of $R$ and $l$ a nonnegative integer.  Assume that corollary (2) holds for all rings $R$ and every integer $k \leq l$.  Then $S^{-1}R$ has dimension at most $l$ iff for any given $x_0, \ldots, x_l \in R$ there exist $a_0,\ldots, a_l \in R$, $s \in S$ and $m_0,\ldots,m_l \in \mathbb{N}$ such that $$x_0^{m_0}(\cdots(x_l^{m_l}(s+a_lx_l)+\cdots) +a_0x_0 ) = 0$$

After proving this, the authors note, the induction is easily completed by specializing $S^{-1}R$ to an appropriate boundary ring and applying Theorem $1$.  
Proof:
First the forward direction.  Suppose $S^{-1}R$ has dimension at most $l$.
Pick $x_0, \ldots, x_l$ in $R$.  Applying the inductive hypothesis to $S^{-1}R$, there exist $s_0, \ldots, s_l \in S, b_0, \ldots, b_l \in R, m_0,\ldots,m_l \in \mathbb{N}$ such that
$$\frac{x_0}{1}^{m_0}\big(\cdots\big(\frac{x_l}{1}^{m_l}\big(\frac{1}{1}+\frac{b_l}{s_l}\frac{x_l}{1}\big)+\cdots\big) +\frac{b_0}{s_0}\frac{x_0}{1} \big) = \frac{0}{1}$$
in $S^{-1}R$.  
Set $s' = \prod_i s_i$ and $b_i' = b_i\prod_{j \not= i} s_i$.  
We can kill denominators by multiplying by $\frac{s'}{1}$ and that gives us
$$\frac{x_0}{1}^{m_0}\big(\cdots\big(\frac{x_l}{1}^{m_l}\big(\frac{s'}{1}+\frac{b_l'}{1}\frac{x_l}{1}\big)+\cdots\big) +\frac{b_0'}{1}\frac{x_0}{1} \big) = \frac{0}{1}$$ in $S^{-1}R$.
Thus there exists some $t \in S$ such that $t x_0^{m_0}(\cdots(x_l^{m_l}(s'+b_l'x_l)+\cdots) +b_0' x_0) = 0$ in $R$.
Setting $s = ts'$ and $a_i = tb_i'$ we get exactly equation (2) from the paper, proving the forward implication.  
For the reverse direction, we are given $\frac{x_0}{t_0}, \ldots, \frac{x_l}{t_l} \in S^{-1}R$ (with $x_i \in R$, $t_i \in S$).  By assumption, 
there exists $b_0, \ldots, b_l \in R$, $s \in S$, $m_0, \ldots, m_l \in \mathbb{N}$ such that $$x_0^{m_0}(\cdots(x_l^{m_l}(s+b_lx_l)+\cdots) +b_0x_0 ) = 0$$ in $R$.  
Considering the image of this equation in $S^{-1}R$ we can divide by $\prod t_i^{m_i + 1}$ and distribute terms as needed in order to restore the proper denominators to all of the $x_i$ terms, allowing the $a_i$ and $s$ terms to absorb the excess.  In the end we're left with something of the form $$\frac{x_0}{t_0}^{m_0}\big(\cdots\big(\frac{x_l}{t_l}^{m_l}\big(s'+b_l'\frac{x_l}{t_l}\big)+\cdots\big) +b_0'\frac{x_0}{t_0} \big) = \frac{0}{1}$$
where $s'$ is a unit in $S^{-1}R$ and $b_i' \in S^{-1}R$.  Multiplying by $s'^{-1}$, and again allowing the $b_i'$ to absorb as necessary, you get a relation like $$\frac{x_0}{t_0}^{m_0}\big(\cdots\big(\frac{x_l}{t_l}^{m_l}\big(1+a_l\frac{x_l}{t_l}\big)+\cdots\big) +a_0\frac{x_0}{t_0} \big) = \frac{0}{1}$$
Since the $\frac{x_i}{t_i}$ were $l$ arbitrary elements of $S^{-1}R$, the inductive hypothesis implies that $S^{-1}R$ has dimension at most $l$.  
