the model provided is a lazy cauchy sequence so any given real number can be computed to arbitrary precision. the theorems about real numbers are directly provable and potentially machine checkable, assuming decidable type checking works out.