Yeah, I always felt like I was either pointlessly restating the obvious or it expected me to derive the damn thing from first principles.
AI slop proof, just because I was curious if duck.ai could do it
Using the natural numbers defined from 0 by the successor operation S:
1=S(0), 2=S(1), ... , 20=S^20^(0), 40=S^40^(0)
Define a < b to mean that there exists a natural number k such that
a+k=b.
Take a=20 and k=20. By repeated addition,
20+20=40.
Since 20 is a natural number, there exists a natural number k such that
20+k=40.
Therefore, by the definition of the ordering relation,
20<40.
(Is it correct? Fuck if I know!)