mathlib3
e71c115f - feat(order/max): no value is accessible in a `no_min_order` / `no_max_order` (#15931)
