proposition: Lemma oap_relP1 u v: related (order_associated r) u v <-> [/\ inc u (quotient (equivalence_associated_o r)) , inc v (quotient (equivalence_associated_o r)) & exists x y, [/\ inc x u, inc y v & related r x y]].
proof: Proof. set s:= equivalence_associated_o r. set p:= graph (canon_proj s). rewrite /order_associated -/s -/p. have es:equivalence s by apply: equivalence_preorder1. split. move /compose3_relP=> [x [y [xu yv xy]]]. have fc: function (canon_proj s) by apply: canon_proj_f. move: (p1graph_source fc xu); aw => xs. move: (p1graph_source fc yv); aw => ys. have: (u = Vf (canon_proj s) x) by apply: Vf_pr. have: (v = Vf (canon_proj s) y) by apply: Vf_pr. rewrite canon_proj_V // canon_proj_V //. move=> -> ->; split; fprops. exists x, y; split => //; first by apply: inc_itself_class. by apply: inc_itself_class. move=> [uq vq [x [y [xu yv xy]]]]; apply /compose3_relP. exists x, y; split => //. apply/(rel_gcp_P es) => //; apply: (inc_in_setQ_sr es xu uq). apply/(rel_gcp_P es) => //; apply: (inc_in_setQ_sr es yv vq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)