mathlib

75f5289e - feat(data/list/perm): binding all the sublists of a given length gives all the sublists (#15834)

feat(data/list/perm): binding all the sublists of a given length gives all the sublists (#15834) This is essentially the defining relation between `sublists'` and `sublists_len`. This also adds a few other trivial lemmas about `sublists_len`.