x + y ⋖ x + z ↔ y ⋖ z

Stream: Is there code for X?

[Violeta Hernández]

Do we have some variant of this? If not, what are the necessary typeclass hypotheses to prove it?

[Violeta Hernández]

@Yaël Dillies

[Yaël Dillies]

No, we don't have it. The precise condition you need is that (x + ·) is an order embedding. It happens that we don't have a nice set of typeclasses that implies that

[Yaël Dillies]

CovariantClass α α (· + ·) (· ≤ ·) + ContravariantClass α α (· + ·) (· ≤ ·) should do

[Violeta Hernández]

Ehm, do you know what those typeclasses are named now? A recent refactor renamed them

[Daniel Weber]

There's still docs#CovariantClass and docs#ContravariantClass, but I think you can use docs#AddLeftMono and docs#AddLeftReflectLE

[Yaël Dillies]

See #13154