Commit 2022-01-12 07:31 9fd03e1d

chore(order/lexicographic): cleanup (#11299) Changes include:

• factoring out prod.lex.trans from the proof of le_trans in prod.lex.has_le, and similarly for antisymm and is_total
• adding some missing to_lex annotations in the prod.lex.{le,lt}_def lemmas
• avoiding reproving decidability of prod.lex
• replacing some proofs with pattern matching to avoid getting type-incorrect goals where prod.lex.has_le appears comparing terms that are not of type lex.