RingOrder for types with decidable equality

[mdgeorge4153]

I'm interested in working with ordered rings with decidable equality (in particular, I would like to show that the field of fractions of an ordered ring is also ordered in the natural way, and that an ordered commutative ring is an integral domain).

As noted in the comments of interfaces/orders.v, the deeply nested class hierarchy for orders is difficult to work with. The comment says "we will, later on, provide means to go back and forth between the usual classical notions and these constructive notions." but I can't tell whether this connection has been done or how to use it if it has.

Apologies if this is an inappropriate place to ask.

[spitters]

I don't think that has been done, so a PR would be welcome.

[mdgeorge4153]

Sounds good. I'm still a bit new to Coq, but I'll see what I can do.