Consider the set of natural numbers $\mathbb N$. On this set we define an operation '+', as follows: for all $n,m \in \mathbb N$ we put $n+m$ to be the unique natural number $t \in \mathbb N$ such that there are $X,Y$ such that
$$ X \cap Y = \emptyset, \quad X \cup Y = t, \quad X \sim n, \quad Y \sim m.$$
This is called, for obvious reasons, the "cardinal definition" of addition on the natural numbers.
(You can assume that we already know (i.e. we've already proved) that there is such a natural number $t$, and moreover that this number is unique.)
Here '$X \sim n$' means that there is a bijection between $X$ and $n$.
I'm having a lot of trouble proving the following (quite elementary it seems) result:
Theorem. For all $m,n,k \in \mathbb N$ we have $$ n < m \quad \Leftrightarrow \quad n + k < m + k.$$
(Here for any natural numbers $n,m$ we use the abbreviation $n<m$ for $n \in m$.)
Of course one would think that a good first approach would be to go by induction; I've tried it on $k$ but it didn't work out. Well..., it is clear that induction on $k$ 'works' assuming the fact that we already know that $n+(k+1) = (n+k) + 1$ for all natural numbers $n,k$. So it is sufficient to show the latter statement. I've found a proof for it, but ironically in the proof I (have to) use the above (unproved) theorem, namely the implication from left to right. So I'm basically stuck in a circularity.
I also tried several other things, without success.
Comment. You are not allowed to use any 'theorems' about the natural numbers, except for the most basic ones. For example, you may use that they form a linear order, but not much more. Also, at this point there is no such thing as an 'ordinal definition' of the '+' on the natural numbers.