proposition: Lemma compatible_equivalence_preorder1 r u v x y: preorder r -> related r x y -> related (equivalence_associated_o r) x u -> related (equivalence_associated_o r) y v -> related r u v.
proof: Proof. move => pr rxy /eao_P [_ pb] /eao_P [pc _]. move: pr => [_ _ tr]; apply: tr (tr _ _ _ pb rxy) pc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)