Commit 2022-11-11 07:59 27863065

feat(set_theory/ordinal/{basic, arithmetic}): move basic results earlier (#15801) This PR does the following moves:

• Move some lemmas on 0, 1, and successors from arithmetic.lean to basic.lean.
• Move results on the order type from the ordinal.card section to its dedicated section.
• Move the order_bot lemmas much earlier to where the partial order is defined.