proposition: Lemma oap_pr: order_associated r = Vfs ( canon_proj (equivalence_associated_o r) \ftimes (canon_proj (equivalence_associated_o r))) r.
proof: Proof. set (s:= equivalence_associated_o r). have es:equivalence s by rewrite /s; apply: equivalence_preorder1. have ss:substrate s = substrate r. by rewrite /s equivalence_associated_o_sr. have fep: function (ext_to_prod (canon_proj s) (canon_proj s)). by apply: ext_to_prod_f; apply: canon_proj_f. have gi: sgraph (Vfs (ext_to_prod (canon_proj s) (canon_proj s)) r). move=> t /dirim_P [x xr Jg]. by move:(p2graph_target fep Jg); rewrite lf_target; move/setX_P => []. apply/sgraph_exten=> //; first by apply: oap_graph. move=> u v; split. move/oap_relP2=> [uq vq hyp]; apply/dirim_P;exists (J (rep u) (rep v)). by apply: hyp; apply: (setQ_repi es). have: (J u v = J (class s (rep u)) (class s (rep v))) by rewrite ! class_rep. rewrite - ext_to_prod_rel_V; fprops; move =>->. by apply: Vf_pr3=> //; rewrite /ext_to_prod; aw; fprops. move/dirim_P=> [x xr Jg]; move: (Vf_pr fep Jg)=> Wx. have px: (pairp x) by move: pr=> [g _ _]; apply: g. have ps: (inc (P x) (substrate s)) by rewrite ss; substr_tac. have qs: (inc (Q x) (substrate s)) by rewrite ss; substr_tac. move: Wx; rewrite -px ext_to_prod_rel_V // => JJ. rewrite (pr1_def JJ) (pr2_def JJ). apply/oap_relP2;split;fprops => a b au bv. suff: (related (order_associated r) (class s (P x)) (class s (Q x))). by move /oap_relP2 => [_ _ h]; apply: h au bv. apply /oap_relP1;split; fprops. exists (P x), (Q x); split ; try apply: (inc_itself_class es) => //. by hnf; rewrite px. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)