mathlib3

1f89414b - Definition of initial ordinals; eliminating superfluous lemma; restoring ordinal.basic