The Coq mailing list

["Lucian M. Patcas" <patcaslm AT mcmaster.ca>]

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?

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

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

Thanks,

Lucian