feat(algebra/order): allow simp to flip inequalities

[semorrison]

We have a constant problem that while a > b is definitionally equal to b < a, tactics that work at the syntactic level can't see this.

This change introduces two simp lemmas, rewriting > and ≥ in terms of < and ≤. This requires a few tweaks elsewhere (essentially places where simp now finishes or comes closer to finishing).

Later, I would like to

1. Just do some general cleanup, replacing lots of > with < in basic files.
2. Start adding @[simp] to many more lemmas about inequalities.
3. Provide substitutes for the default well_founded tactics, which actually break when simp is too good at inequalities. See feat(well_founded_tactics): patch default_dec_tac #1419.

[avigad]

This looks good to me. I'll merge in a day or two if there are no objections.