Commit 2021-12-10 17:07 71e9f90d

feat(order/basic): Slightly generalized densely_ordered (#10664) Changed [preorder α] to [has_lt α].