Or, to say a bit more about this -- I guess the basic principle here is "it's OK to use auxiliaries?" Introducing a larger number system is no different from d

Or, to say a bit more about this -- I guess the basic principle here is "it's OK to use auxiliaries?" Introducing a larger number system is no different from drawing an auxiliary line in geometry (for instance). There's no rule that the proof of a statement may only contain the entities appearing in the statement! You can introduce whatever auxiliaries you like.