proposition: Lemma opposite_order_r r: order_r r -> order_r (opposite_relation r).
proof: Proof. move=> [tr ar rr]. move /opposite_preorder_r: (conj tr rr) => [tr' rr']. by split => // x y xy yx; apply: (ar _ _ yx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)