Fix to the definitions of min and max

[LorenzoMolena]

While working on a future PR, I noticed that when performing a "with-abstraction with UsingEq" on n <ᵇ m, each case was not normalizing to the expected term.
This issue is resolved by adding UsingEq into the definitions of min and max. Interestingly, all proofs that relied on "with-abstraction withot UsingEq" still works unchanged.

I added a comment about this limitation above the definition of UsingEq, but I'm not entirely sure how clear it is, so I also referenced its use in min and max over ℕ.
Please let me know if there is a clearer way to explain this behavior.

[mortberg]

Why not just define min and max by recursion without any with or calls to <?

[mortberg]

So having min (suc n) (suc m) = min n m and similarly for max

[anshwad10]

Why not just define min and max by recursion without any with or calls to <?

They made it like this in #1262 for efficiency, because the _<ᵇ_ builtin is faster than recursing

[anshwad10]

Also, I think this is precisely the advantage of using inspect over UsingEq, because when using inspect we abstract on the value of n <ᵇ m and the path separately

[mortberg]

Ah right, I had forgotten about that. I wonder how much one should worry about efficiency for functions on unary nat though... If we want things to be fast we should at least have a binary representation?

[anshwad10]

Ah right, I had forgotten about that. I wonder how much one should worry about efficiency for functions on unary nat though... If we want things to be fast we should at least have a binary representation?

I don't know if that would help; It wouldn't be better in terms of storage at least, because Agda compiles Nat to built in arbitrary-precision binary integers, and idt it would speed up arithmetic because the builtin operations are O(1) while binary arithmetic is O(logN)

[marcinjangrzybowski]

@mortberg this is part of work to enable fast operations on Integers -> Rationals -> and finaly beeing able to quickly calculatate things like Nth digit of e in #1182 :)
@LorenzoMolena identified bootlenecks, and we have very promising experiments.
We discussed those plans with @felixwellen , but are happy to meet @mortberg to get the feedback on our plan.
With @LorenzoMolena , we will be doing code sprint hopefully integrating this work, 2 weeks from now during AIM.

[LorenzoMolena]

@mortberg I realized that I haven't actively participated in the discussion so far, which may have unintentionally given the impression that this PR is not yet ready to be merged.
The points raised by @anshwad10 and @marcinjangrzybowski are correct: I intentionally chose this definition based on a boolean comparison (which is linked to a builtin) in order to achieve better performance. I tested this approach, and it indeed results in an improvement.

Anyway, those changes have already been merged previously. In this PR, I am only adding an additional UsingEq to the definitions, in order to make some proofs easier to write. As an example of this can be found in this case distinctions in #1276.

In my view, the one remaining aspect that might need review is the new comment above the definition of UsingEq.
If that also sounds clear to you, then I believe this should be ready to merge.