Strict monotonicity of the grid enumeration $x_L = (L \bmod m_1) + M\lfloor L/m_1 \rfloor$ for $M \ge m_1$

This lemma shows that the formula $x_L$ enumerates the grid $\{u + Mj\}$ in increasing order.

Let $m_1 \ge 1$ and $M \ge m_1$ be natural numbers, and for $L \in \mathbb{N}$ let $x_L = (L \bmod m_1) + M \lfloor L/m_1 \rfloor$, so that $x_L = u + Mj$ when $L = j m_1 + u$ with $0 \le u \le m_1 - 1$. Then the map $L \mapsto x_L$ is strictly increasing on $\mathbb{N}$:

Consequently, for every $m_2$, the numbers $x_0 < x_1 < \dots < x_{m_1 m_2 - 1}$ are the elements of the grid $X = \{u + Mj : 0 \le u \le m_1 - 1,\ 0 \le j \le m_2 - 1\}$ in increasing order, and the lifted sequence of the Lift bundle is the jump sequence $\Delta X$, with positive entries. The prefix-sum formula for the lifted sequence, the lift lemma and the lower bound $L(n) \ge m_1 m_2$ rely on this.

Formalization Note The conclusion is Mathlib's StrictMono (liftPrefix m₁ M), over all of $\mathbb{N}$; the note uses it only for $0 \le L \le m_1 m_2 - 1$.