mathlib

019df1c0 - feat(order/max): equivalence of no_top_order and no_max_order for linear orders (#16341)