proposition: Lemma Exercise1_2f3 r r' f g (s := (equivalence_associated f)): increasing_fun f r r' -> composable g (canon_proj s) -> f = compose g (canon_proj s) -> (order_morphism g (quotient_order r s) r' <-> (Ex1_2_hD r f /\ Ex1_2_hD' r r' f)).
proof: Proof. move => incf cgf fc. have qoa:= (Exercise1_2f1 incf). move: incf => [or or' [ff sr sr'] icf]. have [es ss]:= (graph_ea_equivalence ff). have sssr: substrate s = substrate r by rewrite ss. have pr: preorder r by apply: order_preorder. have qp: forall x, inc x (quotient s) -> (inc (rep x) (source f) /\ Vf f (rep x) = Vf g x). move=> x xq; move: (rep_i_sr es xq) => rxs. split; first by rewrite - ss. move: (canon_proj_V rxs); rewrite class_rep // => cpv. have rsc: inc (rep x) (source (canon_proj s)) by aw. by rewrite - {2} cpv - compfV // - fc. have bpP :forall x, inc x (quotient s) -> forall a, (inc a x <-> [/\ inc (rep x) (source f), inc a (source f) & Vf f (rep x) = Vf f a]). move=> x xq a; split. by move=> ax; move: (related_rep_in_class es xq ax); move /(ea_relatedP ff). by move=> h;rewrite -(class_rep es xq); apply /(class_P es) /(ea_relatedP ff). have ax: preorder_quo_axioms r s by split. split => om. have aux: forall y, inc y (source f) -> [/\ inc (class s y) (quotient s), Vf f (rep (class s y)) = Vf g (class s y) & Vf f (rep (class s y)) = Vf f y]. move => y ; rewrite - ss => ys. have csyq:= (inc_class_setQ ys);have p2 := proj2 (qp _ csyq). by move /(bpP _ csyq): (inc_itself_class es ys) => [_ _ p5]. have p1: forall x y, inc x (source f) -> inc y (source f) -> gle r' (Vf f x) (Vf f y) -> exists y', [/\ inc y' (source f), gle r x y' & Vf f y = Vf f y']. move=> x y xsf ysf. have xc: (inc x (class s x)) by apply:inc_itself_class=>//;rewrite ss. move: (aux _ xsf)(aux _ ysf) => [csxq p2 p5][csyq p2' p5']. move: om => [q1 q2 [q3 q4 q5]]. rewrite /fiso_prop q4 substrate_quotient_order // => q6P. rewrite -p5 p2 -p5' p2' => /(q6P _ _ csxq csyq) /quotient_orderP [_ _ q7]. move /q7: xc => [u ucy xu]; rewrite - p2'; exists u. by move: ucy => /(bpP _ csyq) [q8 q9 q10]. split. move => x y x' xy x'sf sW. move: (icf _ _ xy); rewrite sW => fxy. have yc: (inc y (source f)) by rewrite sr; order_tac. apply: p1 x'sf yc fxy. move=> x y xsf ysf leW;move: (p1 _ _ xsf ysf leW) => [x0 [p0 p2' p3]]. by exists x; exists x0. move:om=> [CCt DDt]. have oq: (order (quotient_order r s)) by apply: Exercise1_2d. have sg: (source g = quotient s) by move: cgf => [_ _ ->]; aw. have tg: substrate r' = target g by rewrite - sr' fc; aw. have sqo: substrate (quotient_order r s) = source g. by rewrite sg substrate_quotient_order. have icgP: (forall x y, inc x (source g) -> inc y (source g) -> (gle (quotient_order r s) x y <-> gle r' (Vf g x) (Vf g y))). rewrite sg;move=> x y xsg ysg. move: (qp _ xsg) (qp _ ysg) => [rxs <-][rys <-]; split. move /quotient_orderP => [_ _ aux]. move: (aux _ (setQ_repi es xsg)) => [z /(bpP _ ysg) [q1 q2 q3] lerxz]. by rewrite q3; apply: icf. move => h; apply /quotient_orderP; split => // z /(bpP _ xsg) [p4 p5 p6]. move: (DDt _ _ rxs rys h) => [x' [y' [p1 p2 p3]]]. rewrite p1 in p6. move: (CCt _ _ _ p3 p5 p6) => [t [p7 p8 p9]]. exists t=> //;apply /(bpP _ ysg); split => //; ue. have fg //: function g by fct_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)