[ libs ] Add `public export` modifiers to arithmetic inequality proofs

[elkcl]

Description

This PR adds public export modifiers to multiple functions (mostly inequality proofs) in Data.Nat and Data.Nat.Order.Properties, allowing the compiler to reduce them when used in types containing inequalities. It also changes divCeilNZ from covering to total.

Should this change go in the CHANGELOG?

• [x] If this is a fix, user-facing change, a compiler change, or a new paper implementation, I have updated CHANGELOG_NEXT.md (and potentially also CONTRIBUTORS.md).

[mattpolzin]

I've used many of these proofs extensively in rewrites which don't require them to reduce at compile time so mostly out of curiosity would you mind providing a motivating example or two for this change? You've described it in the abstract in the PR description but I'd be interested in seeing how it manifests in an example.

[elkcl]

Sure. For example, in my project I have a datatype FinInc (which is kinda like Fin, but includes the upper bound and is implemented as a Nat and LTE instead of using a successor function like Data.Fin.Fin) and some arithmetic functions on it that manipulate the bounds:

record FinInc n where
    constructor MkFinInc
    val : Nat
    prf : LTE val n

divCeilNZBounds : (a : Nat) -> (b : Nat) -> (n : Nat) -> (0 nz : NonZero b) -> LTE a (n * b) -> LTE (divCeilNZ a b nz) n

divCeilFlipWeak : {n : Nat} -> {r : Nat} -> (b : Nat) -> (0 _ : NonZero b) => (a : FinInc (minus (n * b) r)) -> FinInc n
divCeilFlipWeak b @{nz} (MkFinInc va pa) = MkFinInc (divCeilNZ va b nz) (divCeilNZBounds va b n nz (transitive pa (minusLTE r (n * b))))

These functions are then used in a different dependent type, and some FinInc arithmetic is performed in the types of its constructors (not in rewrite rules), making it important for certain bounds to be equal, and that requires being able to compute them at compile time. It's kind of hard to make a minimal illustrative example here, but I did have issues with Idris not being able to solve certain constraints until I made at least divCeilNZ and minusLTE public export.

[gallais]

Given this type is proof irrelevant, I don't think we should make the exact shape of the proofs part of the module interface.