My first proof that uses the well-ordering principle (very simple number theory). Please mark/grade.

What do you think about my first proof that uses the well-ordering principle? Please mark/grade.


Theorem

The sum of the cubes of three consecutive natural numbers is a multiple of 9.

Proof

First, introducing a predicate $P$ over $\mathbb{N}$, we rephrase the theorem as follows. $$\forall n \in \mathbb{N}, P(n) \quad \text{where} \quad P(n) \, := \, n^3 + (n + 1)^3 + (n + 2)^3 \text{ is a multiple of 9}$$ We prove the theorem by contradiction. To that end, in step 1, we start by assuming that the negation of the theorem holds. Then, in step 2, we show that some natural number satisfies our predicate. In step 3, we move along with the help of the well-ordering principle. Finally, in step 3, we deduce our contradiction.

Step 1: Assuming the negation
We assume the negation of the theorem: There is a $n \in \mathbb{N}, \neg P(n)$. With that said, we are done as soon as a contradiction is deduced.

Step 2: Satisfying our predicate
Consider the natural number $0$. Since $0^3 + (0 + 1)^3 + (0 + 2)^3 = 0 + 1 + 8 = 9$, we see that $P(0)$ is true.

Step 3: Employing the well-ordering principle
By our assumption, there is a natural number for which the predicate is false. Thus there is a non-empty set of such numbers. According to the well-ordering principle, the set contains a least element $k$. Since $P(0)$ is true, we infer that $k \ne 0$, more precisely $k > 0$. Hence, $k - 1$ is a natural number; and by choice of $k$, we have that $P(k - 1)$ is true.

Step 4: The contradiction
As $P(k - 1)$ is true, there is a natural number $i$ such that $$i \cdot 9 = (k - 1)^3 + k^3 + (k + 1)^3\text{.}$$ We use this fact in the following equivalent transformation. In the transformation, the first line does not represent a multiple of $9$, since $P(k)$ is false; however, the last line clearly does represent a multiple of $9$. This is our contradiction, which completes the proof.

\begin{align} k^3 + (k + 1)^3 + (k + 2)^3 &= (k - 1)^3 + k^3 + (k + 1)^3 + (k + 2)^3 - (k - 1)^3 \\ &= (k - 1)^3 + k^3 + (k + 1)^3 + k^3 + 6k^2 + 12k + 8 - k^3 + 3k^2 - 3k + 1 \\ &= (k - 1)^3 + k^3 + (k + 1)^3 + 9k^2 + 9k + 9 \\ &= 9i + 9k^2 + 9k + 9 \\ &= 9 \cdot (i + k^2 + k + 1) \end{align}


While I have no objection to the proof as such, this problem seems to me to be an example in which the machinery of well-ordering/induction is unnecessary, and avoiding it leads to a much shorter proof. $n^3 + (n+1)^3 + (n+2)^3 = 3n^3 + 9n^2 + 15n + 9 \equiv 3n^3-3n$ (mod 9). This latter will be congruent to 0 mod 9 so long as $n^3 - n \equiv 0$ (mod 3). But $n^3-n = (n-1)n(n+1)$ and one of any three consecutive numbers is divisible by 3.