how do I activate `sum.lex`?

Stream: Is there code for X?

[Scott Morrison]

Are there some defs somewhere that I can local attribute [instance] to turn on sum.lex as a preorder/partial_order/...?

[Scott Morrison]

(i.e. assuming the corresponding structure on both sides of the sum?)

[Yury G. Kudryashov]

It seems that sum.lex takes two relations as arguments. I can't find any lemmas about sum.lex being preorder etc