On Fri, 8 Jan 2010, Adam Naumowicz wrote:
If that is the only problem, you just need a reservation saying that natural numbers are also real numbers, so that the definition of ^2 can be matched - use XREAL_0 for that.
A 'registration', not a 'reservation', of course :-) Adam