Description: Define class of all ordered fields. An ordered field is a field with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 18-Jan-2018)