Noetherian semiring is proper.

Our first main result is Theorem \[CubProp\] below, where we show properness of the cubic functors ${{\ensuremath{F_{\,{\mathbb S}}}}}$ on , for $\mathbb S$ being one of the semirings $\mathbb N$, $\mathbb Q_+$, $\mathbb R_+$, and of the cubic functor ${{\ensuremath{F_{\,{[0,1]}}}}}$ on . The case of ${{\ensuremath{F_{\,{\mathbb N}}}}}$ is known from [@beal.lombardy.sakarovitch:2006 Theorem 4] [^3], the case of ${{\ensuremath{F_{\,{[0,1]}}}}}$ is stated as an open problem in [@milius:2017 Example 3.19].

\[CubProp\] The cubic functors ${{\ensuremath{F_{\,{\mathbb N}}}}}$, ${{\ensuremath{F_{\,{\mathbb Q_+}}}}}$, ${{\ensuremath{F_{\,{\mathbb R_+}}}}}$, and ${{\ensuremath{F_{\,{[0,1]}}}}}$ are proper.

In fact, for any two coalgebras with free finitely generated carrier and any two elements having the same trace, a zig-zag with free and finitely generated nodes relating those elements can be found, which is a span (has a single intermediate node with outgoing arrows).

The proof proceeds via relating to the Noetherian case. It always follows the same scheme, which we now outline. Observe that the ring completion of each of $\mathbb N$, $\mathbb Q_+$, $\mathbb R_+$, is Noetherian (for the last two it actually is a field), and that $[0,1]$ is the positive part of the unit ball in $\mathbb R$.

*Step 1. The extension lemma:*  We use an extension of scalars 