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.
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
