Enriched Orders

[anshwad10]

I define pre- and partial orders enriched in an ordered monoid, and I show that these generalize unenriched pre- and partial orders by enriching in the lattice Prop. I also use these to define biorders/antithesis orders by enriching in antithesis propositions.
In the future (once we have real numbers) I can use these to define Lawvere metric spaces.
I might also define enriched ring ideals and enriched ordered monoids and rings (these would generalize the 'admissible ordered fields' as defined in the HoTT Book).