proposition: Lemma orsum_directed: (right_directed (order_sum r g) <-> (right_directed r /\ forall i, maximal r i -> right_directed (Vg g i))).
proof: Proof. move: (oa) => [or sr alo]. have os: order (order_sum r g) by fprops. have srr:= (orsum_sr oa). split. move /right_directedP => [oor h]; split. apply /right_directedP;split => // x y xsr ysr. move: (orsum_pr0 xsr) => [x0 p1 p2]. move: (orsum_pr0 ysr) => [y0 p3 p4]. rewrite - srr in p2 p4. move: (h _ _ p2 p4) => [z [ zx zy]]. move: (orsum_gle_id oa zx) (orsum_gle_id oa zy); aw=> q1 q2. by exists (Q z); split => //; move:(du_index_pr1 zs); rewrite sr; case. move=> i []; rewrite sr => isr im. apply /right_directedP; split;fprops;move=> x y xsi ysi. move: (disjoint_union_pi1 isr xsi)(disjoint_union_pi1 isr ysi) => p1 p2. rewrite - srr in p2 p1. move: (h _ _ p1 p2) => [z [le1 le2]]. move:(arg2_sr le1); rewrite srr => /du_index_pr1 [p3 p4 p5]. move: (orsum_gle_id oa le1); aw => /im Qzi. move: le1 => /orsum_gleP [_ _];rewrite /order_sum_r Qzi. case; [ by case; aw | aw;move => [ _ le1]]. move: le2 => /orsum_gleP [_ _]; rewrite /order_sum_r Qzi. case; [ by case; aw | aw;move => [ _ le2]]. exists (P z); split => //; ue. move => [ /right_directedP [_ rr] imr]; apply /right_directedP; split => //. move=> x y xsr ysr; rewrite srr in xsr ysr. move: (du_index_pr1 xsr) (du_index_pr1 ysr) => [Qx Px px][Qy Py py]. rewrite - sr in Qx Qy; move: (rr _ _ Qx Qy) => [z [ Qxz Qyz]]. case: (equal_or_not (Q x) z) => eQxz; case: (equal_or_not (Q y) z) => eQyz. + case: (p_or_not_p (maximal r z)) => mz. - move: (imr _ mz); move: (proj1 mz); rewrite sr => zs. move /right_directedP => [oz etc]. rewrite eQxz in Px;rewrite eQyz in Py. move: (etc _ _ Px Py)=> [t [ t1 t2]]. have aux:inc (J t z) (sum_of_substrates g). by apply: disjoint_union_pi1 => //; apply: (arg2_sr t1). exists (J t z);split => //; apply /orsum_gleP=> //; rewrite/order_sum_r pr1_pair pr2_pair; split=> //; right;split => //;ue. - have [u us zu]: (exists2 u, inc u (substrate r) & glt r z u). ex_middle h; case: mz; split => //; first by ue. move=> t zt; case: (equal_or_not z t) => // nzt. by case: h; exists t=> //; order_tac. move: (orsum_pr0 us) => [v v1 v2]; exists (J v u); split; apply /orsum_gleP=> //; rewrite /order_sum_r ?eQxz ?eQyz; aw; split;fprops. + exists x; split => //; first by order_tac; rewrite orsum_sr. apply /orsum_gleP; split => //; left; rewrite eQxz; split => //. + exists y; split => //; last by order_tac; rewrite orsum_sr. apply /orsum_gleP; split => //;left; rewrite eQyz; split => //. + move:(arg2_sr Qxz) => zdg. move: (orsum_pr0 zdg) => [v v1 v2]; exists (J v z); split; apply /orsum_gleP; split => //; left; aw; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)