mathlib3

13b9478e - feat(combinatorics/colex): introduce colexicographical order (#4858)

feat(combinatorics/colex): introduce colexicographical order (#4858) We define the colex ordering for finite sets, and give a couple of important lemmas and properties relating to it. Part of #2770, in order to prove the Kruskal-Katona theorem. Co-authored-by: Alena Gusakov <agusakov@udel.edu>