mathlib3

refactor(set_theory/ordinal): shorten proof of well_ordering_thm

#1078

Merged