#line 371 "/home/travis/build/felix-lang/felix/src/packages/algebra.fdoc"
  // total order
  class Tord[t]{
    inherit Eq[t];
    // defined in terms of <, argument order swap, and boolean negation
  
    // less
    virtual fun < : t * t -> bool;
    fun lt (x:t,y:t): bool=> x < y;
    fun \(\lt\) (x:t,y:t): bool=> x < y;
    fun \(\lneq\) (x:t,y:t): bool=> x < y;
    fun \(\lneqq\) (x:t,y:t): bool=> x < y;
  
  
    axiom trans(x:t, y:t, z:t): x < y and y < z implies x < z;
    axiom antisym(x:t, y:t): x < y or y < x or x == y;
    axiom reflex(x:t, y:t): x < y and y <= x implies x == y;
    axiom totality(x:t, y:t): x <= y or y <= x;
  
  
    // greater
    fun >(x:t,y:t):bool => y < x;
    fun gt(x:t,y:t):bool => y < x;
    fun \(\gt\)(x:t,y:t):bool => y < x;
    fun \(\gneq\)(x:t,y:t):bool => y < x;
    fun \(\gneqq\)(x:t,y:t):bool => y < x;
  
    // less equal
    fun <= (x:t,y:t):bool => not (y < x);
    fun le (x:t,y:t):bool => not (y < x);
    fun \(\le\) (x:t,y:t):bool => not (y < x);
    fun \(\leq\) (x:t,y:t):bool => not (y < x);
    fun \(\leqq\) (x:t,y:t):bool => not (y < x);
    fun \(\leqslant\) (x:t,y:t):bool => not (y < x);
  
  
    // greater equal
    fun >= (x:t,y:t):bool => not (x < y);
    fun ge (x:t,y:t):bool => not (x < y);
    fun \(\ge\) (x:t,y:t):bool => not (x < y);
    fun \(\geq\) (x:t,y:t):bool => not (x < y);
    fun \(\geqq\) (x:t,y:t):bool => not (x < y);
    fun \(\geqslant\) (x:t,y:t):bool => not (x < y);
  
    // negated, strike-through
    fun \(\ngtr\) (x:t,y:t):bool => not (x < y);
    fun \(\nless\) (x:t,y:t):bool => not (x < y);
  
    fun \(\ngeq\) (x:t,y:t):bool => x < y;
    fun \(\ngeqq\) (x:t,y:t):bool => x < y;
    fun \(\ngeqslant\) (x:t,y:t):bool => x < y;
  
    fun \(\nleq\) (x:t,y:t):bool => not (x <= y);
    fun \(\nleqq\) (x:t,y:t):bool => not (x <= y);
    fun \(\nleqslant\) (x:t,y:t):bool => not (x <= y);
  
  
    // maxima and minima
    fun max(x:t,y:t):t=> if x < y then y else x endif;
    fun \(\vee\)(x:t,y:t) => max (x,y);
  
    fun min(x:t,y:t):t => if x < y then x else y endif;
    fun \(\wedge\)(x:t,y:t):t => min (x,y);
  
  
  }