lex_has_le

Dictionary / lexicographic ordering on pairs.

lex_preorder

Dictionary / lexicographic preorder for pairs.

lex_partial_order

Dictionary / lexicographic partial_order for pairs.

lex_linear_order

Dictionary / lexicographic linear_order for pairs.

lex_decidable_linear_order

Dictionary / lexicographic decidable_linear_order for pairs.

dlex_has_le

Dictionary / lexicographic ordering on dependent pairs.

The 'pointwise' partial order prod.has_le doesn't make sense for dependent pairs, so it's safe to mark these as instances here.

dlex_preorder

Dictionary / lexicographic preorder on dependent pairs.

dlex_partial_order

Dictionary / lexicographic partial_order for dependent pairs.

dlex_linear_order

Dictionary / lexicographic linear_order for pairs.

dlex_decidable_linear_order

Dictionary / lexicographic decidable_linear_order for dependent pairs.