Add two cites to HoTT for ordered fields iset.mm
Add two cites to HoTT for ordered fields iset.mm

This is the source we've been using for definition of an ordered
field in iset.mm. Here we reference ltmul1 and reaplt which means
we have nine of the ten parts of Definition 11.2.7(vi). The tenth
is lemul1a in set.mm but we don't have it yet.

metamath/set.mm,metamath/set.mm,metamath/set.mm