OrderIso from StrictMono

Stream: Is there code for X?

[Violeta Hernández]

Do we have that a strictly monotone equiv (between linear orders) is an OrderIso?

[Bhavik Mehta]

docs#StrictMono.orderIsoOfRightInverse

[Violeta Hernández]

Just found that myself. It's pretty close to what I want, though I think the Equiv version would still be a useful corollary to have.

[Violeta Hernández]

Oh nvm, just using StrictMono.orderIsoOfRightinverse is indeed simpler for what I'm doing.