[Merged by Bors] - feat(Order/WellFoundedSet): minimal element of a nonempty set exists if < is well founded on the set#39777

Hagb wants to merge 4 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

WuProver:WellFoundedOn-minimalWuProver/mathlib4:WellFoundedOn-minimalCopy head branch name to clipboard