proposition: Theorem worder_merge g (G := unionb g): common_worder_axiom g -> [/\ (common_extension_order g G), worder G, (forall a x, inc a (domain g) -> segmentp (Vg g a) x -> segmentp G x), (forall a x, inc a (domain g) -> inc x (substrate (Vg g a)) -> segment (Vg g a) x = segment G x) & (forall x, segmentp G x -> x = substrate G \/ exists2 a, inc a (domain g) & segmentp (Vg g a) x)].
proof: Proof. move=> co. move: (order_merge4 co)=>coe. move: coe=> [oh sh Vag]. move: co => [pb pc pd]. have p1: (forall a, inc a (domain g) -> sub (substrate (Vg g a)) (substrate G)). by move=> a adg; rewrite sh; move=> t ts; apply: (setUf_i adg). have p0 a x y: inc x (substrate (Vg g a)) -> gle G y x -> inc y (substrate G) -> inc a (domain g) -> inc y (substrate (Vg g a)). move => xs yx ys adg. move: (setUf_hi yx) => [u udg Jv]. case: (pc _ _ adg udg) => h; first by apply:(proj1 h); substr_tac. exact: (proj2 h _ _ xs Jv). have p2: (forall a, inc a (domain g) -> segmentp G (substrate(Vg g a))). move=> a adg;split; first by apply: p1. move=> x y xs yx;exact: (p0 a _ _ xs yx (arg1_sr yx) adg). have p3:(forall a x, inc a (domain g) -> inc x (substrate (Vg g a)) -> segment (Vg g a) x = segment G x). move=> a x adg xs; set_extens y => ys; move: (inc_segment ys) => [yx nyx]. apply /segmentP; split=>//; apply: setUb_i adg yx. apply/segmentP; split => //;rewrite (Vag _ adg);apply/iorder_gle0P => //. exact: (p0 a _ _ xs yx (arg1_sr yx) adg). have p4: (forall a x, inc a (domain g) -> segmentp (Vg g a) x -> segmentp G x). move=> a x adg sa; case: (well_ordered_segment (pb _ adg) sa). by move=> ->; apply: p2. by move=> [y ysV ->]; rewrite (p3 _ _ adg ysV); apply: segment_segment. have p5: worder G. apply:(worder_prop_rev oh) => x xsr [y yx]. move: (xsr _ yx)=> ysr; rewrite sh in ysr. move: (setUf_hi ysr) => [a adg ysVa]. set (x1:= x \cap (substrate (Vg g a))). have sx1s: (sub x1 (substrate (Vg g a))) by apply: subsetI2r. have nx1: nonempty x1 by exists y; apply: setI2_i. move: (worder_prop (pb _ adg) sx1s nx1)=> [z zs zle]. have zx: inc z x by apply: (setI2_1 zs). have zVa: inc z (substrate (Vg g a)) by apply: (setI2_2 zs). exists z => // t tx. move: (xsr _ tx); rewrite sh => tu; move: (setUf_hi tu)=> [b bdg bV]. have aux: inc t (substrate (Vg g a)) -> gle G z t. move=> hyp. by move:(zle _ (setI2_i tx hyp));rewrite (Vag _ adg) => /iorder_gle1. case: (pc _ _ adg bdg); move => [p p']; first by apply: (aux (p _ bV)). move: (p _ zVa)=> zVb. case: (total_order_pr2 (worder_total (pb _ bdg)) bV zVb). move=> [tz ntz]; apply: (aux (p' _ _ zVa tz)). rewrite Vag // => h; exact:(iorder_gle1 h). split => //. move=> x seg. case: (well_ordered_segment p5 seg); [ by left | move=>[y ysr ->]; right ]. rewrite sh in ysr; move: (setUf_hi ysr)=> [a adg ap]; ex_tac. rewrite -(p3 _ _ adg ap); apply: segment_segment (proj1 (pb _ adg)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)