mathlib3

4538aeb2 - feat(data/finset/fold): add lemma `fold_max_add` (#15257)

feat(data/finset/fold): add lemma `fold_max_add` (#15257) The lemma shows that adding inside or outside a "max-fold" amounts to the same. It is the folded version of docs#max_add_add_right.