Splitting the Segment [m+n] into [m] and a Shifted Copy of [n]

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, let $m,n\in\mathbb{N}$, with $+$, $<$ and $\le$ as in Arithmetic and Order of the Natural Numbers, intervals $\{a,\dots,b\}$ and segments $[p]$ for $a,b,p\in\mathbb{N}_{0}$ as in Intervals of Natural Numbers §interval and Intervals of Natural Numbers §segment, and differences $b-a$ for $a,b\in\mathbb{N}_{0}$ with $a\le b$ as in The Difference of Two Natural Numbers with Zero §difference.

¶ $m+n\in\mathbb{N}$ and $[m]\subseteq[m+n]$.

¶ For every $j\in[n]$, $m+j\in[m+n]$ and $m+j\notin[m]$. The map $[n]\to[m+n]\setminus[m]$, $j\mapsto m+j$, is a bijection.

¶ Every $k\in[m+n]$ lies in exactly one of the sets $[m]$ and $\{m+j:j\in[n]\}$, the latter being the set of values of the map of the clause shift. If $k$ lies in the second set, then $m<k$, $k-m\in[n]$, $k=m+(k-m)$, and $j=k-m$ is the only $j\in[n]$ with $k=m+j$.