Theorem: Dipper Operation is Associative

Let $m, n \in \Z$ be integers such that $m \ge 0, n > 0$.
Let $\N_{< \paren {m \mathop + n} }$ denote the initial segment of the natural numbers:
:$\N_{< \paren {m \mathop + n} } := \set {0, 1, \ldots, m + n - 1}$
The '''dipper operation''' on $\N_{< \paren {m \mathop + n} }$ is associative.

Proof:
Recall the definition of the '''dipper operation''' on $\N_{< \paren {m \mathop + n} }$ defined as:
:$\forall a, b \in \Z_{>0}: a +_{m, n} b = \begin{cases} a + b & : a + b < m \\ a + b - k n & : a + b \ge m \end{cases}$
where $k$ is the largest integer satisfying:
:$m + k n \le a + b$
Let $a, b, c \in \N_{< \paren {m \mathop + n} }$ be arbitrary.
There are a number of cases to address.
By Dipper Operation is Commutative it is possible to arrange $a$, $b$ and $c$ into any order, and the result of $\paren {a +_{m, n} b} +_{m, n} c$ and $a +_{m, n} \paren {b +_{m, n} c}$ will be unaffected.
{{WLOG}}, therefore, it is sufficient to consider the scenario where $a \le b \le c$.
;Case 1: Let $a + b + c < m$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {a +_{m, n} b} +_{m, n} c
      | r = \paren {a + b} + c
      | c = Definition of $+_{m, n}$
}}
{{eqn | r = a + \paren {b + c}
      | c = Natural Number Addition is Associative
}}
{{eqn | r = a +_{m, n} \paren {b +_{m, n} c}
      | c = Definition of $+_{m, n}$
}}
{{end-eqn}}
Otherwise $a + b + c \ge m$.
;Case 2: Let $a + b < m$ and $b + c < m$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {a +_{m, n} b} +_{m, n} c
      | r = \paren {a + b} +_{m, n} c
      | c = Definition of $+_{m, n}$
}}
{{eqn | r = \paren {a + b} + c - k n
      | c = Definition of $+_{m, n}$
      | cc= where $k = \max \set {k: m + k n \le \paren {a + b} + c}$
}}
{{eqn | r = a + \paren {b + c} - k n
      | c = Natural Number Addition is Associative
      | cc= where $k = \max \set {k: m + k n \le a + \paren {b + c} }$
}}
{{eqn | r = a +_{m, n} \paren {b + c}
      | c = Definition of $+_{m, n}$
}}
{{eqn | r = a +_{m, n} \paren {b +_{m, n} c}
      | c = Definition of $+_{m, n}$
}}
{{end-eqn}}
;Case 3: Let $a + b < m$ and $b + c \ge m$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {a +_{m, n} b} +_{m, n} c
      | r = \paren {a + b} +_{m, n} c
      | c = Definition of $+_{m, n}$
}}
{{eqn | r = \paren {a + b} + c - k n
      | c = Definition of $+_{m, n}$
      | cc= where $k = \max \set {k: m + k n \le \paren {a + b} + c}$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = a +_{m, n} \paren {b +_{m, n} c}
      | r = a +_{m, n} \paren {b + c - k_1 n}
      | c = Definition of $+_{m, n}$
      | cc= where $k_1 = \max \set {k: m + k n \le b + c}$
}}
{{eqn | r = \begin {cases} a + \paren {b + c - k_1 n} & : a + \paren {b + c - k_1 n} < m \\ a + \paren {b + c - k_1 n} - k_2 n & : a + \paren {b + c - k_1 n} \ge m \end {cases}
      | c = Definition of $+_{m, n}$
      | cc= where $k_2 = \max \set {k: m + k n \le a + \paren {b + c - k_1 n} }$
}}
{{eqn | r = a + \paren {b + c} - k n
      | c = 
      | cc= where $k = \max \set {k: m + k n \le a + \paren {b + c} }$
}}
{{eqn | r = \paren {a + b} + c - k n
      | c = Natural Number Addition is Associative
      | cc= where $k = \max \set {k: m + k n \le \paren {a + b} + c}$
}}
{{end-eqn}}
;Case 4: Let $a + b \ge m$ and $b + c \ge m$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {a +_{m, n} b} +_{m, n} c
      | r = \paren {a + b - k_1 n} +_{m, n} c
      | c = Definition of $+_{m, n}$
      | cc= where $k_1 = \max \set {k: m + k n \le a + b}$
}}
{{eqn | r = \begin {cases} \paren {a + b - k_1 n} + c & : \paren {a + b - k_1 n} + c < m \\  \paren {a + b - k_1 n} + c - k_2 n & : \paren {a + b - k_1 n} + c \ge m \end {cases}
      | c = Definition of $+_{m, n}$
      | cc= where $k_2 = \max \set {k: m + k n \le \paren {a + b - k_1 n} + c}$
}}
{{eqn | r = \paren {a + b} + c - k n
      | c = 
      | cc= where $k = \max \set {k: m + k n \le \paren {a + b} + c}$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = a +_{m, n} \paren {b +_{m, n} c}
      | r = a +_{m, n} \paren {b + c - k_1 n}
      | c = Definition of $+_{m, n}$
      | cc= where $k_1 = \max \set {k: m + k n \le b + c}$
}}
{{eqn | r = \begin {cases} a + \paren {b + c - k_1 n} & : a + \paren {b + c - k_1 n} < m \\ a + \paren {b + c - k_1 n} - k_2 n & : a + \paren {b + c - k_1 n} \ge m \end {cases}
      | c = Definition of $+_{m, n}$
      | cc= where $k_2 = \max \set {k: m + k n \le a + \paren {b + c - k_1 n} }$
}}
{{eqn | r = a + \paren {b + c} - k n
      | c = 
      | cc= where $k = \max \set {k: m + k n \le a + \paren {b + c} }$
}}
{{eqn | r = \paren {a + b} + c - k n
      | c = Natural Number Addition is Associative
      | cc= 
}}
{{end-eqn}}
So in all cases:
:$\paren {a +_{m, n} b} +_{m, n} c = a +_{m, n} \paren {b +_{m, n} c}$
and the result follows by definition of associative operation.
{{qed}}