proposition: Lemma Exercise1_2i r s (q := quotient s) (r' := quotient_order r s) (f' := identity_g q) (g' := Lg q (fun z => induced_order r z)) (du := disjointU f') (f := Lf (fun x => J x (class s x)) (substrate r) du): weak_order_compatibility r s-> Ex1_2_hC' r s -> total_order r -> [/\ orsum_ax r' g', (forall i, inc i (domain g') -> nonempty (substrate (Vg g' i))), substrate (order_sum r' g') = du, (forall x y, inc x (substrate r) -> inc y (substrate r) -> (related s x y <-> related (equivalence_associated (second_proj du)) (Vf f x) (Vf f y)))& order_isomorphism f r (order_sum r' g')].
proof: Proof. move=> woc qoa tor. move: (Exercise1_2g woc qoa tor) (Exercise1_2h woc qoa tor)=> p1 [p2 p3]. move: woc tor => [[ps es sr] woc'] [or tor]. have sr': (substrate r' = q) by rewrite /r' substrate_quotient_order //. have iqs: (forall i, inc i q -> sub i (substrate r)). move=> i iq t ti; rewrite - sr;apply: (inc_in_setQ_sr es ti iq). have oa1: orsum_ax r' g'. rewrite /g';saw. hnf;aw;move=> i iq; rewrite LgV//; move: (iqs _ iq) => h. apply: (proj1 (iorder_osr or h)). have oa2: (forall i : Set, inc i (domain g') -> nonempty (substrate (Vg g' i))). rewrite /g'; aw; move=> i iq; rewrite LgV//; move: (iqs _ iq) => h. rewrite iorder_sr //; apply: (setQ_ne es iq). have sos: substrate (order_sum r' g') = du. rewrite orsum_sr // /du /sum_of_substrates /f' /fam_of_substrates. rewrite /g';aw; apply: f_equal; apply: Lg_exten => x xd /=. rewrite LgV// iorder_sr//; fprops. have ta: lf_axiom (fun x => J x (class s x)) (substrate r) du. move=> t tr /=. have ts: inc t (substrate s) by ue. have tc: inc t (class s t) by apply:inc_itself_class => //. apply: disjointU_pi; rewrite /f'. rewrite identity_d; apply /(setQ_P es); apply: class_class => //. by rewrite /identity_g LgV//; apply: inc_class_setQ. have bf: bijection f. rewrite /f;apply: lf_bijective => //. move=> u v _ _ sj; apply: (pr1_def sj). move=> y ydu; move: (disjointU_hi ydu). rewrite /f' /identity_g Lgd; move=> [qy]; rewrite LgV// => Py py. move: ((iqs _ qy) _ Py) => psr; ex_tac; apply: pair_exten; aww. apply: is_class_pr => //. have tf: du = target f by rewrite /f; aw. have sf: substrate r = source f by rewrite /f; aw. have du1: du = sum_of_substrates g' by rewrite - sos orsum_sr //. split => //. move=> x y xsr ysr. have sxx:related s x x by rewrite - sr in xsr;equiv_tac. rewrite du1 -/(E13_S _) /f LfV//; split. move => sxy; apply/(Exercise1_3a6P g'); rewrite LfV// ;split => //. by rewrite /E13_sF -du1; apply: ta. by rewrite /E13_sF -du1; apply: ta. by move /(related_equiv_P es): sxy => [_ _]; aw. move /(Exercise1_3a6P g'); move => [_ _]; rewrite LfV//; aw => h. apply /(related_equiv_P es);split => //; ue. split => //; fprops. saw; ue. red; rewrite - sf; move=> x y xsf ysf; rewrite /f !LfV//. have Jx: inc (J x (class s x)) du by apply: ta. have Jy: inc (J y (class s y)) du by apply: ta. rewrite - sr in xsf ysf. have cxq: inc (class s x) q by apply: inc_class_setQ. have cyq: inc (class s y) q by apply: inc_class_setQ. have xcx: inc x (class s x) by apply:inc_itself_class. have ycy: inc y (class s y) by apply:inc_itself_class. have sxx:related s x x by equiv_tac. split. move => rxy; apply /orsum_gleP; rewrite -du1;split => //. case: (p_or_not_p (related s x y)) => sxy. have aux: class s x = class s y by apply: class_eq1. right;saw; rewrite /g' LgV//; apply /iorder_gle0P => //; ue. left; aw;split; last by dneg xx; apply /(related_equiv_P es). apply /quotient_orderP; split => //. move=> z /(class_P es) sxz; move: (woc' x y z rxy sxz)=> [t syt rzt]. by exists t=> //; apply /(class_P es). move /orsum_gleP => [_ _]; case; last first. move=> [_]; aw; rewrite /g' LgV// => h; apply: (iorder_gle1 h). aw; move => [] /quotient_orderP [q1 q2 h] necc. move: (h _ xcx) => [z zc xz]. rewrite sr in xsf ysf;case: (tor _ _ xsf ysf) => // yx. case: necc; apply: (class_eq1 es). apply: (symmetricity_e es);move: zc => /(class_P es) zc. apply: (qoa y x z yx xz zc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)