mathlib

c4ef20e9 - feat(order/rel_classes): an irreflexive order on a subsingleton type is a well order (#14601)

feat(order/rel_classes): an irreflexive order on a subsingleton type is a well order (#14601) This generalizes a previously existing lemma that the empty relation on a subsingleton type is a well order.