The Coq mailing list

[CHAUVIN Barnabe <barnabe.chauvin AT gmail.com>]

Hello club !

I am currently trying to prove (this is just for practice) a 
mathematical (it is not intented to be extracted) theorem : prove that 
the density of a set A in the reals set.
I'm not sure at all about the english of this, but here is the 
mathematical proposition : 
http://latex.codecogs.com/gif.latex?%5Cforall%20x%2C%20y%20%5Cin%20%5Cmathrm%7BA%7D%2C%20x%20%3C%20y%20%5CRightarrow%20%5Cexists%20z%20%5Cin%20%5Cmathbb%7BQ%7D%2C%20x%20%3C%20z%20%3C%20y 


I define the set A as a subset of R (I actually use a sigma-type)
I tought I could write a predicate is_dense that depends on two 
PartialOrder : 
https://coq.inria.fr/library/Coq.Sets.Partial_Order.html#PO  (I was 
thinking of this because it provides the sets (the carriers) and the 
order relation on this sets, but it might be a bad idea. Don't hesitate 
to advise me better practices)
The problem is that I don't want to redefine another order relation for 
my subset A (which is a subset of R that already have order relations) : 
I would like the coercions from A to R be automated ...  Is it possible ?

Best regards,