The Coq mailing list

["Lucian M. Patcas" <lucian.patcas AT gmail.com>]

Hello,

I have these positive reals: 

Variable delta : posreal.
Variable x : nonnegreal.

and my development has propositions such as:

exists n : N, x = n * delta.

which don't type check as n does not have type R.  How should I deal with this?

Thanks,
Lucian