proposition: Lemma opposite_preorder_r r: preorder_r r -> preorder_r (opposite_relation r).
proof: Proof. rewrite /preorder_r/opposite_relation; move => [tr rr]. split; [by move=> x y z xy yz; apply: tr yz xy | by move=> x y /rr [] ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)