perf: a isDefEq friendly Fin.sub

[leodemoura]

The performance issue at #4413 is due to our Fin.sub definition.

def sub : Fin n → Fin n → Fin n
  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + (n - b)) % n, mlt h⟩

Thus, the following runs out of stack space

example (a : UInt64) : a - 1 = a :=
  rfl

at the isDefEq test

(a.val.val + 18446744073709551615) % 18446744073709551616 =?= a.val.val

From the user's perspective, this timeout is unexpected since they are using small numerals, and none of the other Fin basic operations (such as Fin.add and Fin.mul) suffer from this problem.

This PR implements an inelegant solution for the performance issue. It redefines Fin.sub as

def sub : Fin n → Fin n → Fin n
  | ⟨a, h⟩, ⟨b, _⟩ => ⟨((n - b) + a) % n, mlt h⟩

This approach is unattractive because it relies on the fact that Nat.add is defined using recursion on the second argument.

The impact on this repo was small, but we want to evaluate the impact on Mathlib.

closes #4413

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-4421 build failed against this PR. (2024-06-11 02:15:32) View Log
• 💥 Mathlib branch lean-pr-testing-4421 build failed against this PR. (2024-06-11 03:13:30) View Log
• ❌ Mathlib branch lean-pr-testing-4421 built against this PR, but the archive failed. (2024-06-11 05:51:48) View Log
• ❌ Mathlib branch lean-pr-testing-4421 built against this PR, but the archive failed. (2024-06-11 18:18:58) View Log