proposition: Theorem isomorphism_worder_alt r r': worder r -> worder r' -> let iso:= (fun u v f => segmentp v (Imf f) /\ order_morphism f u v) in (exists! f,iso r r' f) \/ (exists! f, iso r' r f).
proof: Proof. move=> wor wor' iso. set (E:= substrate r). set (E':= substrate r'). have or: order r by fprops. have or': order r' by fprops. move: (extension_osr E E'). set o1:= (extension_order E E'); set o2:= opp_order o1. move => [oe soe1]; move: (opp_osr oe) => [ooe osr]. have soe: sub_functions E E' = substrate o2 by ue. set (s:= (Zo (sub_functions E E') (fun z => exists2 u, segmentp r u & iso (induced_order r u) r' z))). have ssee: sub s (sub_functions E E') by rewrite /s; apply: Zo_S. have sse: sub s (substrate o1) by ue. have ssoxee: sub s (substrate o2) by ue. have ins:inductive (induced_order o2 s). move=> X;rewrite (iorder_sr ooe ssoxee) => Xs;rewrite(iorder_trans _ Xs)=> pX. have Xse:sub X (sub_functions E E') by apply: (sub_trans Xs ssee). have Xsoe:sub X (substrate o2) by ue. have alseg: forall x, inc x s -> segmentp r (source x). move=> x /Zo_hi [u ru [_ bb]]; move: bb => [_ _ [_ -> _] _]. by rewrite iorder_sr //;apply: sub_segment1. have alsegr: forall x, inc x s -> segmentp r' (Imf x). by move=> x /Zo_hi [u _ [sv _]]. have Xso: sub X (substrate o1) by ue. move: pX => [_ ]; rewrite iorder_sr // => ppX. have cov: forall u v x, inc u X -> inc v X -> inc x (source u) -> inc x (source v) -> Vf u x = Vf v x. move=> u v x uX vX xsu xsv. move: (ppX _ _ uX vX); case => h; move: (iorder_gle1 h); move/igraph_pP/ extension_orderP => [_ _ h0]; [ | symmetry];apply: extends_sV => //. move:(sup_extension_order2 Xse cov)=> [x [lubx sx rgx gx]]. move: lubx => /(lubP ooe Xsoe) [[xsoe xb] lub]; rewrite - soe in xsoe. suff xs: inc x s. exists x; split; first by rewrite iorder_sr //. move=> y yX; move: (Xs _ yX)=> ys. by apply /iorder_gle0P => //; apply: xb. have ssx: segmentp r (source x). rewrite sx; apply: setUf_segment. by hnf; aw;move=> a aX; rewrite LgV//;apply: alseg; apply: Xs. rewrite /s; apply: Zo_i=>//; exists (source x) => //. have srgx: segmentp r' (Imf x). rewrite rgx; apply: setUf_segment. by hnf;aw;move=> a aX; rewrite LgV//;apply: alsegr; apply: Xs. have sxsr: sub (source x) (substrate r) by move: ssx=> []. have srxs: sub (Imf x) (substrate r') by move: srgx => []. have xi: (forall a b, inc a (source x) -> inc b (source x) -> (gle (induced_order r (source x)) a b <-> gle r' (Vf x a) (Vf x b))). move=> a b; rewrite sx => asX bsX. apply: (iff_trans(iorder_gle0P r asX bsX)). move: (setUf_hi asX)=> [u uX]. move: (setUf_hi bsX)=> [v vX]. rewrite Lgd in uX vX; rewrite !LgV// => bv au. have [w [wX asw bsw]] :exists z, [/\ inc z X, inc a (source z) & inc b (source z)]. move: (ppX _ _ uX vX) ; case => h; move: (iorder_gle1 h); move/igraph_pP/ extension_orderP => [_ _ ext]; move: (extends_Ssource ext)=> sext. by move: (sext _ au) => ax; exists v. by move: (sext _ bv) => ax; exists u. rewrite - (extension_order_pr (xb _ wX) asw). rewrite - (extension_order_pr (xb _ wX) bsw). move:(Xs _ wX) => /Zo_hi [z [sz _ [_ [_ _ [_ sf _] ifz]]]]. rewrite (iorder_sr or sz) in sf; rewrite - sf in ifz. split; last by move /(ifz _ _ asw bsw);apply:iorder_gle1. move => lab; apply /(ifz _ _ asw bsw);apply/(iorder_gleP ) => //. move: xsoe => /sfunctionsP [fx srcx tx]. move: (iorder_osr or srcx) => [pa pb]. done. move:(iorder_osr ooe ssoxee) => [oio sio]. move: (Zorn_lemma oio ins) => [f []]; rewrite iorder_sr // =>fis fmax. move: (fis) => /Zo_P [fee [x sx xiso]]. case: (equal_or_not x (substrate r)) => h. move: xiso; rewrite h iorder_substrate //; move=> xiso. left; apply /unique_existence;split; first by exists f. move=> a b [s1 m1][s2 m2]. by apply: (isomorphism_worder_unique (r:=r) (r':=r')). right; apply /unique_existence;split; last first. move=> a b [s1 m1][s2 m2]. by apply: (isomorphism_worder_unique (r:=r') (r':=r)) =>//. case: (equal_or_not (Imf f) (substrate r'))=> h'. move: xiso => [_ xiso]; move: (order_morphism_fi xiso) => injf. set (g:= triple E' E (inverse_graph (graph f))). move: xiso=> [_ _ [ff sf tf] vf]. have gf: sgraph (graph f) by fprops. have sf': source f = x by rewrite sf iorder_sr //; apply: sub_segment1. have rgg: range (graph g) = x. by rewrite /g; aw; rewrite igraph_range // domain_fg. have fg: function g. rewrite /g; apply: function_pr. split;fprops; move=> a b /=. move/igraphP=> [pa J1g] /igraphP [pb J2g] sv. rewrite - sv in J2g; move: (injective_pr3 injf J1g J2g). by apply: pair_exten. by move: rgg; rewrite /g; aw; move=> ->;move: sx=> [xe _]. by rewrite igraph_domain // -(ImfE ff). exists g. hnf; rewrite (ImfE fg) rgg /order_morphism;split => //. split => //; first by split => //;try solve [ rewrite /g; aw;trivial]. move=> a b asg bsg. have fgp: (forall u, inc u (source g) -> (inc (Vf g u) (source f) /\ Vf f (Vf g u) = u)). move=> u usg; move: (Vf_pr3 fg usg); rewrite {2} /g; aw. move/igraph_pP => Jg; split; [ Wtac | symmetry;apply: (Vf_pr ff Jg)]. move: (fgp _ asg)(fgp _ bsg)=> [W1s va][W2s vb]. rewrite -{1} va -{1} vb. rewrite - (vf _ _ W1s W2s); split; first (by apply:iorder_gle1). move => lab; apply/iorder_gle0P => //; ue. case: (well_ordered_segment wor sx)=> aux; first by case:h. move: aux=> [a asr xa]. move: xiso=> [st [_ _ [ff sf tf] isf]]. case: (well_ordered_segment wor' st)=> aux; first by case:h'. move: aux=> [b vsr tb]. set (g:=extension f a b). have sfx: source f = x by rewrite sf iorder_sr // xa; apply: sub_segment. have asf: ~ (inc a (source f)) by rewrite sfx xa; move;apply: not_in_segment. have fg:function g by apply: extension_f. have tg: target g = E'. rewrite/g /extension; aw; rewrite tf; by apply: setU1_eq. have sg: source g = segmentc r a. by rewrite /g/extension; aw; rewrite sfx xa; apply: segmentc_pr. have sap t: sub (segmentc r t) (substrate r) by apply: Zo_S. have rgg: (Imf g = segmentc r' b). rewrite (ImfE fg) /g/extension; aw; rewrite - segmentc_pr // range_setU1. by rewrite - (ImfE ff) tb. have gs: inc g s. rewrite /s; apply: Zo_i. by apply/sfunctionsP;split => //; rewrite sg; apply: sap. exists (segmentc r a). by apply: segmentc_segment. split; first by rewrite rgg; apply: segmentc_segment. move: (iorder_osr or (sap a)) => []; rewrite - sg => pa pb. hnf;split => // u v; rewrite sg - segmentc_pr //. move => qa qb; apply: (iff_trans (iorder_gle0P r qa qb)). move: qa qb; rewrite - xa - sfx => /setU1_P ut /setU1_P vt. have p1: forall w, inc w (source f) -> glt r' (Vf f w) b. move=> w wsf. have: inc (Vf f w) (Imf f) by Wtac. by rewrite tb; move/segmentP. have p2: forall w, inc w (source f) -> glt r w a. by move=> w; rewrite sfx xa; move/segmentP. case: ut => hu; [rewrite extension_Vf_in // | rewrite hu extension_Vf_out //]. case:vt => hv;[rewrite extension_Vf_in // | rewrite hv extension_Vf_out //]. move:(isf u v hu hv). move:(iff_sym(iorder_gle0P r hu hv)); rewrite sfx. move => qa qb; exact: (iff_trans qa qb). by move: (p1 _ hu)(p2 _ hu)=> [e1 _][e2 _]. case:vt => hv; [rewrite extension_Vf_in // | rewrite hv extension_Vf_out //]. move: (p1 _ hv)(p2 _ hv)=> [e1 ne1][e2 ne2]. split => h'';[ case: ne2 | case: ne1];order_tac. by split => _; order_tac. have eqfg: g = f. have pa: inc g (sub_functions E E') by rewrite /g/extension; fprops. have pb: sub (graph f) (graph g) by rewrite corresp_g;fprops. have pc: sub (target f) (target g) by rewrite corresp_t ; fprops. apply: fmax; apply /iorder_gle0P => //; apply /igraph_pP. by apply /extension_orderP. case: asf; rewrite -eqfg sg. by apply: inc_bound_segmentc. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)