Commit 2022-10-24 07:29 99d31295

feat(data): port finsupp.ne_locus/lex to dfinsupp (#16777)

• Add new files dfinsupp/ne_locus and dfinsupp/lex mostly by copying the finsupp counterparts and making trivial adaptions. Use the dfinsupp lemmas/constructions to golf the finsupp counterpart, e.g. the linear_order on finsupp.lex.
• Add lemmas lex_lt_of_lt(_of_preorder) for each of pi/finsupp/dfinsupp that shows the (<) relation on the product of a family of partial orders is a subrelation of the lexicographic (<), for any choice of well-founded relation (in the case of pi) or strict total order (in the case of (d)finsupp) on the set of coordinates. Useful to deduce well-foundedness of the product order from the well-foundedness of the lexicographic order in #16772.