proposition: Lemma equivalence_preorder r: preorder_r r -> equivalence_r (symmetrize r).
proof: Proof. move=> [ tr _]; split; first by move=> x y [rxy ryx]. move=> x y z [xy yx] [yz zy]; split; [ apply: tr xy yz | apply: tr zy yx]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)