Definition of OrderedCommRing

[LorenzoMolena]

The definition is adapted from ordered fields present in the HoTT Book (defn 11.2.7).
This also adds a pseudolattice type with structure. The property was already encoded in Poset.Properties, but the record was missing.

[anshwad10]

Thanks! (this is to resolve #1181 i presume?)

[LorenzoMolena]

@anshwad10 the motivation was independent, but sure this provides ordered comm. rings, aiding with #1181.
Do you find this defn. reasonable?

[anshwad10]

@LorenzoMolena This is a good definition 👍
However, on second thought, I think antithesis partial orders are useful in their own right, so maybe you could define something like a biordered set which has both a strict and non-strict ordering, and then put the weakening and bimodule laws in that?
Not that important though, this is enough

[mortberg]

Looks good to me! Merging