mathlib

eb024dc8 - feat(order/lexicographic): lexicographic pre/partial/linear orders (#820)

feat(order/lexicographic): lexicographic pre/partial/linear orders (#820) * remove prod.(*)order instances * feat(order/lexicographic): lexicographic pre/partial/linear orders * add lex_decidable_linear_order * identical constructions for dependent pairs * cleaning up * Update lexicographic.lean forgotten `instance` * restore product instances, and add lex type synonym for lexicographic instances * proofs in progress * * define lt * prove lt_iff_le_not_le * refactoring