A while ago I wondered about how Proof Assistants like Coq prove $m \leq n$ and the like. It looks like they actually need to traverse the natural numbers based on the successor/predecessor formulation:
Coq < Eval compute in le_lt_dec 100000 1000000.Warning: Stack overflow or segmentation fault happens when working with large numbers in nat (observed threshold may vary from 5000 to 70000 depending on your system limits and on the command executed). Stack overflow.
One of the answers suggested using the BinInt (Binary Integers representation) to perform this operation.
When a mathematician looks at a claim like $1000 ≤ 1000000$ and says "obviously", they are taking advantage of the fact that we wrote the claim in decimal notation. If you want to do something similar in CoQ, you could try to prove, e.g., $10∗10∗10≤10∗10∗10∗10∗10$.
So I'm wondering if there is a standard way of representing numbers as types without defining them like Peano's axioms style, using successor/predecessor and the like. Something that allows you to prove two numbers have a relation such as $m \leq n$ or $m \neq n$ or do other common things with numbers like adding/subtracting, in such a way where the "formal definition" (i.e. succ/pred) of the numbers is combined with some more computationally optimal version so you can use it in practice. Not sure what best-practice is to do here, but I would like to define a numbers type and have it gain all the advantages of proof theory / proof assistants, while also being the actual type definition used to construct i.e. integers.