Design patterns of hierarchies for order structures

Stream: general

[Trebor Huang]

I didn't read the whole paper, but since mathlib is mentioned I thought I'd post it here. Is it (the problem and the solution, separately) applicable to mathlib?

[Eric Wieser]

Notation "x ≤ y" := (@le nat_display _ x y).
Notation "x %| y" := (@le dvd_display _ x y).

is an interesting take on "I want two different lattice structures on a single type", but I think it's not particularly novel; it's been discussed before WRT replacing to_additive I believe, and dismissed as not a great solution (as the lemma names end up still being weird for the less canonical instance)