The Coq mailing list

[Fr�d�ric Besson <frederic.besson AT inria.fr>]

Hi,

You can either:

* inject N into R
   Apparently, this is not part of the library.

  Definition IBinNatR (n:N) : R :=
  match n with
    | N0 => IZR 0%Z
    | Npos p => IZR (Zpos p)
  end.

* use Peano integers instead of N
  Raxioms.INR : nat -> R injects nat into R

I would favor option 2...

Best,
--
Frédéric Besson


On 28 juil. 2011, at 08:09, Lucian M. Patcas wrote:

> 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