feat: add binary search shrinking for numeric types

[alok]

Adds shrinkToMinimal for numeric types using binary search.

Problem: Nat.shrink only tries n/2, n/4, ... so for test n ≥ 50 from 4096, it finds 64.

Solution: Binary search finds true minimal (50).

Nat.shrink (iterative): 4096 → 64
Nat.shrinkToMinimal:    4096 → 50

Adds: Nat.binarySearch, *.shrinkToMinimal for Nat, Int, Fin, UInt8/16/32/64

Termination proven via termination_by hi - lo.

[tom93]

Hi, I came across this PR while browsing, I have a comment about this PR and a broader comment about Plausible's current integer shrinking:

• This code in this PR does not appear to have integration with the Shrinkable instances, so it would not get used with Plausible.Testable.check, am I correct? It would be nice to to have minimal integer shrinking everywhere (see the next comment).

• In the current Shrinkable implementation, the candidates for n are [n/2, n/4, n/8, ..., 0]. This doesn't make sense to me, because if n/2 fails there is no point trying n/4 (assuming the proposition is monotonic). QuickCheck's shrinkIntegral uses the candidates [0, n-n/2, n-n/4, n-n/8, ..., n-1], which gives minimal shrinking; why not use that?