mathlib3

ed2cfce8 - feat(set_theory/ordinal/basic): tweak theorems on order type of empty relation (#14650)

feat(set_theory/ordinal/basic): tweak theorems on order type of empty relation (#14650) We move the theorems on the order type of an empty relation much earlier, and golf them. We also remove other redundant theorems. `zero_eq_type_empty` is made redundant by `type_eq_zero_of_empty`, while `zero_eq_lift_type_empty` is made redundant by the former lemma and `lift_zero`.