Ordinal/Basic vs Ordinal/Arithmetic

Stream: mathlib4

[Violeta Hernández]

Currently, Ordinal/Basic is split a bit weird, containing some results on addition but missing a lot of other important things that are relegated to the start of Ordinal/Arithmetic. The docstring claims:

we only introduce [addition] and prove its basic properties to deduce the fact that the order on ordinals is total (and well founded).

But after #16401, ordinal addition is required for neither of those things.

[Violeta Hernández]

Ordinal addition is required for the SuccOrder instance, since succ x is defined as x + 1. But maybe there's a case for that being moved as well.

[Violeta Hernández]

Here's the thing though - Ordinal/Basic is too weak of an import for almost anything involving ordinals. The only other files that import Ordinal/Basic but not Ordinal/Arithmetic are Ordinal/Arithmetic itself, and Cardinal/UnivLE for Cardinal.univ, which really should have been defined as #Cardinal and been placed in Cardinal/Basic.

[Violeta Hernández]

Also, Ordinal/Basic is 1450 lines long, while Ordinal/Arithmetic clocks in at a whopping 2500 :confused:

[Violeta Hernández]

So clearly these files should be split, but I'm unclear on what the best way to do it is

[Violeta Hernández]

Here's an idea I have: split Arithmetic into Arithmetic and Order. Define addition, subtraction, successors, multiplication, and division in the former. Move all the stuff about infima and suprema to the latter.