proposition: Lemma compatible_equivalence_preorder r (s := symmetrize r): preorder_r r -> forall x y x' y', r x y -> s x x' -> s y y' -> r x' y'.
proof: Proof. move=> [tr _] x y x' y' rxy [rxx' rx'x] [ryy' ry'y]. move: (tr _ _ _ rx'x rxy) => rx'y. apply: tr rx'y ryy'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)