What Tonio did is an example of what is called in some texts "synthetic proof". Notice that he started from the thing he wanted to prove and manipulated it to a statement that is "trivially" true. Strictly speaking, you are not allowed to assume what you want to prove but here everything is "reversible" (note the double ended arrows). The "real" proof would start from , which is obviously true because x< y, and work backwards to .