You would need to get to the reals, which takes already a fair amount of time and includes a lot of machinery. Depending on how you constructed the reals, you might be able to reuse some concepts. So, it depends on where you start and which path you take.

Also, arguing by reference to the choice of appropriate values is incomplete argumentation and so it won't be accepted by a formal system. You'd have to fill these holes.

I'd suggest to start by evaluating the existing formalized constructions of the reals.

I think it is not too hard.