proposition: Lemma oap_relP2 u v: related (order_associated r) u v <-> [/\ inc u (quotient (equivalence_associated_o r)), inc v (quotient (equivalence_associated_o r)) & forall x y, inc x u -> inc y v -> related r x y].
proof: Proof. set (s:= equivalence_associated_o r). have es: equivalence s by rewrite /s; apply: equivalence_preorder1. split. move /oap_relP1 => [uq vq [x [y [xu yv xy]]]]; split=> //. move=> a b au bv. have xa: (related s x a). by apply /(in_class_relatedP es); exists u; split => //;apply/(setQ_P es). have yb: (related s y b). by apply /(in_class_relatedP es); exists v;split => //; apply/(setQ_P es). apply: (compatible_equivalence_preorder1 pr xy xa yb). move => [uq vq hyp]; apply/oap_relP1;split => //. move: (setQ_repi es uq) (setQ_repi es vq) => pa pb. by exists (rep u); exists (rep v);split => //; apply: hyp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)