feat(set_theory/ordinal/arithmetic): Add missing instances for `ordinal` (#14128)
We add the following instances:
- `monoid_with_zero ordinal`
- `no_zero_divisors ordinal`
- `is_left_distrib_class ordinal`
- `contravariant_class ordinal ordinal (swap (+)) (<)`
- `is_antisymm ordinal (∣)`