fact: Definition sort (x y: A) : A * A := if decide_rel (≤) x y then (x, y) else (y, x).
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.orders MathClasses.orders.lattices MathClasses.theory.setoids