mathlib3

463089da - feat(order/rel_classes): A total relation is trichotomous (#9181)