proposition: Lemma oap_osr: order_on (order_associated r)(quotient (equivalence_associated_o r)).
proof: Proof. have ea:equivalence (equivalence_associated_o r). by apply: equivalence_preorder1. set eao:= (equivalence_associated_o r). have prop: forall a b, inc (J a b) (order_associated r)-> (inc a (quotient eao) /\ inc b (quotient eao)). move=> a b Jab. have: (related (order_associated r) a b) by done. by move/oap_relP2=> [pa pb _]. have sr:substrate (order_associated r) = quotient eao. set_extens x. move:(@oap_graph r) => h. by move/(substrate_P h) => [][y /oap_relP2 [pa pb _]]. move=> xq; apply: (arg1_sr (y:=x));apply/oap_relP2; split => // z y zx yx. suff: symmetrize (gle r) z y by move => []. apply/eao_P; apply/(in_class_relatedP ea). by exists x;split => //; apply/(setQ_P ea). have go: sgraph (order_associated r) by apply: oap_graph. split => //. move:(pr)=> [rr gr tr]; split => //. hnf; rewrite sr => y ys;apply/oap_relP2; split => // x z xy zy. have: (related (equivalence_associated_o r) x z). by apply/(in_class_relatedP ea); exists y; split=>//; apply/(setQ_P ea). by move/eao_P=> []. move=> x y z /oap_relP2 [xq yq rxy]/oap_relP2 [_ zq ryz]. apply/oap_relP2;split => // a b ax bz; move: (setQ_repi ea yq) => cy. apply: tr (rxy _ _ ax cy) (ryz _ _ cy bz). move=> x y /oap_relP2 [xq yq rxy] /oap_relP2 [_ _ ryx]. move:(setQ_repi ea xq) (setQ_repi ea yq) => ax biy. move: (rxy _ _ ax biy)(ryx _ _ biy ax)=> rab rba. move: (conj rab rba); move /eao_P=> reab. move: xq yq => /(setQ_P ea) cx /(setQ_P ea) cy. have bx: inc (rep y) x by apply: (rel_in_class2 ea cx reab). case: (class_dichot ea cx cy) =>// hyp. case: (nondisjoint bx biy hyp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)