[Merged by Bors] - feat(Order/WellFounded): the minimum of f '' s is f applied to the minimum of s#38992

SnirBroshi wants to merge 2 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

SnirBroshi:feature/order/well-founded-min-imageSnirBroshi/mathlib4:feature/order/well-founded-min-imageCopy head branch name to clipboard