 Leading-coefficient proof for a central polynomial extension

For a right ideal $I\subseteq R[t]$, let $L_d$ be the set of degree-$d$ coefficients of its elements of degree at most $d$. These are right ideals of $R$, and multiplication by the central variable makes $L_d\subseteq L_{d+1}$. They stabilize, and every $L_d$ before stabilization is finitely generated. Choose polynomial lifts of those generators. Subtracting a suitable right linear combination of the lifts, shifted by powers of $t$, cancels the leading coefficient of any element of $I$. Induction on degree proves that the finitely many chosen lifts generate $I$.

// Destination: noncommutative-algebra.bigb