* into third argument of STL's sort(). Note that this does not define a
* strict weak ordering since for any symbol x we have neither 3*x<2*x or
* 2*x<3*x. Handle with care! */
* into third argument of STL's sort(). Note that this does not define a
* strict weak ordering since for any symbol x we have neither 3*x<2*x or
* 2*x<3*x. Handle with care! */