Commit 2021-04-09 04:34 6610e8f5

feat(data/fintype): golf, move and dualise proof (#7126) This PR moves fintype.exists_max higher up in the import tree, and golfs it, and adds the dual version, fintype.exists_min. The name and statement are unchanged.