proposition: Lemma orsum_wor r g: worder_on r (domain g) -> worder_fam g -> worder (order_sum r g).
proof: Proof. move=> [wor sr] alw; move: (proj1 wor) => or. have oa: orsum_ax r g by split => // i ie; exact (proj1 (alw _ ie)). apply:(worder_prop_rev (orsum_or oa)); rewrite orsum_sr // => x xs [x0 x0x]. set A := fun_image x Q. have Asr: (sub A (substrate r)). move=> t /funI_P [z zx ->]. rewrite sr;exact (proj31 (du_index_pr1 (xs _ zx))). have neA: nonempty A by exists (Q x0); apply /funI_P; ex_tac. move: (worder_prop wor Asr neA)=> [a aA ale]. set B:= Zo x (fun z => Q z = a). set C := fun_image B P. move: (Asr _ aA); rewrite sr => adg. have Cs: (sub C (substrate (Vg g a))). move=> t /funI_P [z zB ->]. move: zB => /Zo_P [zx] <-; exact (proj32 (du_index_pr1 (xs _ zx))). have neC: nonempty C. move: aA => /funI_P [z zx qz]. by exists (P z); apply /funI_P;exists z => //; apply: Zo_i. move: (worder_prop (alw _ adg) Cs neC)=> [b bC leB]. have Jx: inc (J b a) x. move: bC => /funI_P [z /Zo_P [zx <-] ->]. by rewrite (proj33 (du_index_pr1 (xs _ zx))). have ors: order (order_sum r g) by fprops. ex_tac => c cx. move: (du_index_pr1 (xs _ cx))=> [Qc Pc pc]. apply /orsum_gleP;split; fprops. hnf; rewrite pr1_pair pr2_pair. have QcA: (inc (Q c) A) by apply /funI_P; ex_tac. move: (ale _ QcA) => leac. case: (equal_or_not a (Q c)). move=> aQc; right;split => //. have Pcb: (inc (P c) C) by apply/funI_P; exists c => //; apply: Zo_i. exact: (leB _ Pcb). by move => nac; left. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)