@Marius, so far I agree with your answer in Comment 8.

One suggestion about the notation (but not the content!) of your ideas: I found it helpful to write the ordering as \$$(a , b, c + n) \leq (a + 2n, b + n , c) \$$, for all \$$a,b,c \in \mathbb{N}\$$. Translating this statement using John's meaning for \$$\leq\$$ would give us "We can get \$$a\$$ Hs, \$$b\$$ Os, and \$$(c +n )\$$ H2Os from \$$(a + 2n)\$$ Hs, \$$(b +n)\$$ Os, and \$$c \$$ H2Os". This jives with my understanding of the problem, and it gets rid of having to worry about \$$a \geq 2n\$$ etc! Also reflexivity follows directly from the case where \$$n = 0\$$.

Other than that I couldn't find a way of streamlining the proofs of the different properties we need to prove. I also did a lot of equation manipulation using the rules of addition. Did anyone else find a simplification?