Combinatorics.Composition !4#2043

Stream: mathlib4

[Arien Malec]

I fixed a bunch of easy stuff....

Status of !4#2043

• disjoint_range depends on wlog -- merge when wlog available
• mem_range_embedding_iff has change..at.. issues
• Major nthFoo to get refactoring
• remaining proof issues

[Arien Malec]

From what I saw, the nth to get refactor wants to happen before the remaining proof fixes b/c nth is embedded in a bunch of places...