mathlib

56c9cab5 - feat(data/sigma{lex,order}): Lexicographic and disjoint orders on a sigma type (#10552)

feat(data/sigma{lex,order}): Lexicographic and disjoint orders on a sigma type (#10552) This defines the two natural order on a sigma type: the one where we just juxtapose the summands with their respective order, and the one where we also add in an order between summands.