mathlib

c6a7f300 - refactor(set_theory/ordinal): shorten proof of well_ordering_thm (#1078)

refactor(set_theory/ordinal): shorten proof of well_ordering_thm (#1078) * refactor(set_theory/ordinal): shorten proof of well_ordering_thm§ * Update ordinal.lean * Update ordinal.lean * Update ordinal.lean * Improve readability * shorten proof * Shorten proof