mathlib3

d3bbaeb9 - chore(combinatorics/composition): use `order_embedding` (#5276)

chore(combinatorics/composition): use `order_embedding` (#5276) * use `order_embedding` for `composition.boundary` * use `order_embedding` for `composition.embedding` * add `max_eq_right_iff` etc * golf some proofs