Commit 2021-12-03 12:40 89697a24

feat(data/fintype/order): complete order instances for fintype (#7123) This PR adds several instances (as defs) for fintypes:

• order_bot from semilattice_inf, order_top from semilattice_sup, bounded_order from lattice.
• complete_lattice from lattice.
• complete_linear_order from linear_order. We use this last one to give a complete_linear_order instance for fin (n + 1) .