I'm also rather confused now notationally, as I thought the convention was that \$$x \le y\$$ means "given x we can get y". But it looks like we might be working in the opposite preorder:

> $x \le x' \textrm{ and } y \le y' \textrm{ imply } x \otimes y \le x' \otimes y' .$
>
> **[...]** if you can get \$$x\$$ from \$$x'\$$ and \$$y\$$ from \$$y'\$$, you should be able to get \$$x\$$ combined with \$$y\$$ from \$$x'\$$ combined with \$$y'\$$.

@[Matthew](https://forum.azimuthproject.org/profile/1818/Matthew%20Doty) wrote:
> For one, we want the following equation to be true:
>
> $$H + O \leq H_2O$$

I think you might mean \$$2H\$$, not \$$H\$$, given that you add your inequalities later and get a \$$3H\$$ term.