The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Le 01/10/2013 07:51, Lucian M. Patcas a écrit :
> Hi,
>
> I have a few questions about real numbers in Coq:
>
> 1. Is there a notation for concrete real numbers in Coq, e.g. how can 
> I write 10.55 in Coq?

There is the Q2R function to convert a rational to a real.

> 2. Is there a theorem or an axiom in the Standard Library that the 
> real numbers are dense? (perhaps I managed to miss it)

What do you mean by dense ? There is the completeness axiom and the 
R_complete theorem that states that every Cauchy sequence converges.

> 3. Is anyone aware of a proof in Coq that the real numbers are dense?
>
> Thanks,
> Lucian

--
JH