Commit 2021-12-04 07:14 3479b7f1

chore(order/complete_lattice): golf a proof (#10607) Also reformulate le_Sup_iff in terms of upper_bounds.