Redefine as many numeric operations in terms of primitive ones as possible

[MatthewDaggitt]

Whilst discussing #581 it came up that several operations in Data.Nat.Base still evaluate using unary arithmetic. In version 2.0 it may be worth fixing these...

• _⊔_
• _⊓_
• ∣_-_∣

[andreasabel]

Do you need more builtins on the Agda side for this? (There are no NATMAX, NATMIN etc. builtins atm.)

[gallais]

I think the plan is to use _<ᵇ_

I suppose this is going to make some Data.Vect.Base definitions more annoying:

alignWith : (These A B → C) → Vec A m → Vec B n → Vec C (m ⊔ n)
restrictWith : (A → B → C) → Vec A m → Vec B n → Vec C (m ⊓ n)