feat: verification of String.toInt?

[TwoFX]

This PR reorganizes the instances ToString Int and Repr Int so that they both point at a common definition Int.repr (the same setup is used for Nat). It then verifies the functions Int.repr, String.isInt and String.toInt.

In particular, for a : Int we get a.repr.toInt? = some a, which implies that Int.repr is injective.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5e1b6ed663d03dccf8beda8352e0822b603dfdd9 --onto 87180a09c49c91577e54284703c73c5ca76be126. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-20 11:12:47)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5e1b6ed663d03dccf8beda8352e0822b603dfdd9 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-20 11:12:49)