feat(Order/WellFoundedSet): a set is finite if both a linear order and its opposite order are well founded on it#39779

Hagb wants to merge 8 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

WuProver:WellFoundedSet-FiniteWuProver/mathlib4:WellFoundedSet-FiniteCopy head branch name to clipboard