proposition: Lemma order_merge3 g: common_worder_axiom g -> common_extension_order_axiom g.
proof: Proof. move=> [alwo pa pb];split => //. by move => w xdg; move: (alwo _ xdg) => [ok _]. move => a b adg bdg;case: (pa _ _ adg bdg); rewrite /segmentp; move => [ss _]; [ exists a | exists b]; split=> //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)