proposition: Lemma orsum_wo_P r g: orsum_ax r g -> allf g ne_substrate -> (worder (order_sum r g) <-> worder r /\ allf^~ worder g).
proof: Proof. move=> oa alne; move:(oa) =>[or sr alog]. split; last by move=> [p1 p2]; apply: orsum_wor => //. move=> h; split; last exact:(orsum_wor_aux oa h). split => // x xsr xne. set (y := fun_image x (fun z => (J (rep (substrate (Vg g z))) z))). have ys: (sub y (substrate (order_sum r g))). rewrite orsum_sr // => t /funI_P. move => [z zx ->]; have zdg: inc z (domain g) by rewrite - sr; apply: xsr. by apply: disjoint_union_pi1 => //; apply: rep_i; apply: alne. have ney: nonempty y by apply: funI_setne. move:h =>[ors wor]. move: (wor _ ys ney) => [z []]; rewrite iorder_sr//; move => zy zle. have Qzx: (inc (Q z) x) by move: zy => /funI_P[t tx ->]; aw. exists (Q z); red; rewrite iorder_sr//; split => //; move=> t tx;apply /iorder_gle0P => //. have py: (inc (J (rep (substrate (Vg g t))) t) y) by apply /funI_P;aw; ex_tac. move: (zle _ py) => le1; move: (iorder_gle1 le1) => le2. by move: (orsum_gle_id oa le2); aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)