mathlib

ac567902 - feat(order/rel_iso): a new definition of order_iso, using preorder instances (#3838)

feat(order/rel_iso): a new definition of order_iso, using preorder instances (#3838) defines (new) `order_embedding` and `order_iso`, which map both < and <= replaces existing `rel_embedding` and `rel_iso` instances preserving < or <= with the new abbreviations