feat(order/hom/basic): `order_iso` of `rel_iso (<) (<)` (#15432)
feat(order/hom/basic): `order_iso` of `rel_iso (<) (<)` (#15432)

We introduce `of_rel_iso_lt` to build an order isomorphism from a relation isomorphism between `(<)` relations. We also add two basic lemmas on `to_rel_iso_lt`.





leanprover-community/mathlib,leanprover-community/mathlib