proposition: Lemma isomorphism_worder_exists r r': worder r -> worder r' -> (exists f, iso_seg_mor r r' f) \/ (exists f, iso_seg_mor r' r f).
proof: Proof. move => wor wor'. have or' := proj1 wor'. have or := proj1 wor. set E' := substrate r'; set E := substrate r. pose T f := the_least (induced_order r' (E' -s (range f))). move: (transfinite_pr1 T wor). set f := transfiniteg_defined r T; move => [fgf df fp]. set A := Zo (substrate r) (fun z => ssub (range (restr f (segment r z))) E'). have sAE: sub A E by apply: Zo_S. pose U x := E' -s range (restr f (segment r x)). have res0 x y: glt r x y -> inc (Vg f x) (range (restr f (segment r y))). move/segmentP => xy;apply/Lg_range_P; ex_tac. have res1: forall x,inc x A -> inc (Vg f x) (U x) /\ (forall y, inc y (U x) -> gle r'(Vg f x) y). move => x /Zo_P [xsr ss1]; move:(setC_ne ss1) => nec. have uE': sub (U x) E' by apply:sub_setC. move:(iorder_osr or' uE') =>[orU srU]. move:(the_least_pr orU (proj2 wor' _ uE' nec)). rewrite (fp _ xsr) /T -/(U x); set u := the_least _; move => []. by rewrite srU => ha hb; split => // y /hb /iorder_gle1. have res2: segmentp r A. split; [ done | move => x y xA le1; apply:Zo_i; first by order_tac ]. move/Zo_P: xA =>[xsr xap]; apply: ssub_trans2 xap. move => t /Lg_range_P [b /segmentP aw ->]; apply: res0; order_tac. have res3 x: inc x A -> inc (Vg f x) E'. by move /res1 /proj1 /setC_P; case. have res4 x y: inc x A -> glt r y x -> glt r' (Vg f y) (Vg f x). move => xA lxy; move:(proj2 res2 x y xA (proj1 lxy)) => yA. have hb b: glt r b x -> (Vg f b) <> (Vg f x). move => lbx eq; move: (proj1 (res1 x xA)); rewrite - eq => /setC_P [_]. by case; apply: res0. move:(res1 y yA) =>[p1 p2]; split; last by apply: hb. apply:p2; apply/setC_P; split; first by apply:res3. move/Lg_range_P => [b /segmentP bry]; apply/nesym; apply: hb; order_tac. have res5 x: inc x A -> inc (Vg f x) (range (restr f A)). move => xA; apply/Lg_range_P; exists x => //. have res6: segmentp r' (direct_image f A). have sA: sub A (domain f) by rewrite df. rewrite -(dirim_restr fgf sA). split; first by move => y/Lg_range_P[b /res3 ok->]. move => x y /Lg_range_P[b bA -> le1]. case: (inc_or_not y (range (restr f (segment r b)))). move => /Lg_range_P [c /segmentP lcb ->]; apply:res5. apply: (proj2 res2 _ _ bA (proj1 lcb)). move => yr. have yU : inc y (U b) by apply/setC_P; split => //; rewrite /E'; order_tac. have ->: y = (Vg f b) by move: (proj2 (res1 _ bA) y yU) => h; order_tac. by apply: res5. case: (emptyset_dichot ((substrate r) -s A)) => ae. move:(extensionality (empty_setC ae) sAE) => EA. set g := triple E E' f. left; exists g; split; first by rewrite /Imf/g /Vfs; aw; rewrite /E EA. apply: (total_order_increasing_morphism (worder_total wor)). have fgg: function_prop g (substrate r) (substrate r'). rewrite /g; saw; apply: function_pr => //. by move => t/(range_gP fgf); rewrite df EA; move => [x /res3 xE ->]. split => // x y lxy; rewrite /g /Vf; aw; apply:res4 => //. rewrite - EA; order_tac. move: (worder_prop wor (@sub_setC E A) ae) => [b bA bp]. move/setC_P: bA => [bE /Zo_P bnA]. have res7 c: glt r c b -> inc c A. move => lcb; have cE: inc c (substrate r) by order_tac. ex_middle bad1; case:(not_le_gt or _ lcb); apply: bp; apply:setC_i; fprops. have rrb: (range (restr f (segment r b))) = E'. ex_middle bad; case:bnA; split => //; split => //. by move => t /Lg_range_P [c /segmentP /res7 lcb ->]; apply: res3. have res8 y: inc y E' -> exists2 x, inc x A & y = Vg f x. rewrite - rrb => /Lg_range_P [c /segmentP /res7 cA ->]; ex_tac. have finj y: inc y E' -> singl_val2 (inc^~ A) (fun x => y = Vg f x). move => yE' u v uA -> vA sv. case: (total_order_pr1(worder_total wor) (sAE _ uA) (sAE _ vA))=> cp. by case:(proj2 (res4 v u vA cp)); rewrite sv. by case:(proj2 (res4 u v uA cp)); rewrite sv. done. pose fi y := select (fun x => y = Vg f x) A. have res9 y: inc y E' -> y = Vg f (fi y) /\ inc (fi y) A. move => yE; apply: (select_pr (res8 _ yE) (finj _ yE)). pose g := Lf fi E' E. have ax: lf_axiom fi E' E by move => t /res9 [_ /sAE]. have sg: source g = E' by rewrite /g;aw. have fg: function g by apply:lf_function. have fgp: function_prop g (substrate r') (substrate r) by rewrite/g; saw. have img: Imf g = A. set_extens t. move/(Imf_P fg); rewrite sg; move=> [u uE ->]. rewrite LfV//; exact: (proj2 (res9 _ uE)). move => tA; move: (res3 _ tA) => ftE. apply/(Imf_P fg); rewrite sg; ex_tac; rewrite LfV//. by apply: (select_uniq (finj _ ftE) tA). right; exists g; split; first by rewrite img. apply: (total_order_increasing_morphism (worder_total wor')). split => // x y lxy. have xE: inc x (substrate r') by order_tac. have yE: inc y (substrate r') by order_tac. rewrite !LfV //; move:(res9 _ xE) (res9 _ yE) => [ha hb] [hc hd]. case: (total_order_pr1(worder_total wor) (sAE _ hb) (sAE _ hd)) => cp //. move: (res4 _ _ hb cp); rewrite - ha - hc => he; order_tac. by case: (proj2 lxy); rewrite ha hc cp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)