proposition: Lemma order_merge1 g: common_extension_order_axiom g -> common_extension_order g (unionb g).
proof: Proof. set G := (unionb g); move=> [alo eVVg pVV]. have gu: sgraph G. by move=> t /setUb_hi [x /alo xdg /(order_sgraph xdg)]. set (E:=unionf (domain g) (fun a => substrate (Vg g a))). have ur: forall y,inc y E -> related G y y. rewrite /E=> y yE; move: (setUf_hi yE)=> [x xdg xp]. by apply: (setUb_i xdg); apply:(proj42 (alo _ xdg)). have su: substrate G = E. set_extens x; last by move=> xE; move: (ur _ xE)=> h; substr_tac. rewrite /E;case /(substrate_P gu) => [] [y Ju]; move: (setUf_hi Ju)=> [z zdg zp]; union_tac; move: (alo _ zdg)=> h; substr_tac. have cov: forall x y, inc x G -> inc y G -> exists u, [/\ inc u (domain g), inc x (Vg g u)& inc y (Vg g u)]. move=> x y xu yu. move: (setUf_hi xu) (setUf_hi yu)=> [a adg ap][b bdg bp]. move: (eVVg _ _ adg bdg)=> [c [cdg sac sbc]]. move:(pVV _ _ adg cdg sac)(pVV _ _ bdg cdg sbc)=> Vag Vbg. move: ap bp; rewrite Vag Vbg /induced_order; aw. by move /setI2_P => [p1 _] /setI2_P [p2 _]; exists c. have oG: order G. split => //. by hnf; rewrite su. rewrite /related => x y z p1 p2. move: (cov _ _ p1 p2)=> [c [cdg p1c p2c]]. move: (alo _ cdg) => or; rewrite /G /related; union_tac; order_tac. rewrite /related => x y p1 p2. move: (cov _ _ p1 p2)=> [c [cdg p1c p2c]]. move: (alo _ cdg)=> or; order_tac. split=>// a adg;set_extens x => xs. apply/setI2_P; split; first by rewrite /G; union_tac. by apply:(sub_graph_coarse_substrate (proj41 (alo _ adg))). move: (setUb_hi (setI2_1 xs))=> [z zdg zpr]. move: (eVVg _ _ adg zdg)=> [t [tdg sa sz]]. rewrite (pVV _ _ adg tdg sa); apply/setI2_P;split;last by apply: (setI2_2 xs). by move: zpr; rewrite(pVV _ _ zdg tdg sz); move/setI2_P => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)