proposition: Lemma osum_increasing1 r f g: orsum_ax r f -> orsum_ax r g -> (forall x, inc x (domain f) -> (Vg f x) <=O (Vg g x)) -> (order_sum r f) <=O (order_sum r g).
proof: Proof. move => oa oa1 ale. have o1: order (order_sum r f) by fprops. have o2: order (order_sum r g) by fprops. split => //; apply: (proj33 (order_le_alt o1 o2 _)). set si:= fun j => choose (fun x => order_morphism x (Vg f j) (Vg g j)). have sip: forall j, inc j (domain f) -> order_morphism (si j) (Vg f j) (Vg g j). move=> j jdf; move:(ale _ jdf) => [p1 p2 [f0 [x [ fx1 fx2]]]]. move: (isomorphism_to_morphism p1 p2 fx1 fx2) => [res _]. rewrite /si; apply choose_pr. by exists (Lf (fun z => Vf f0 z) (substrate (Vg f j)) (substrate (Vg g j))). have dfdg: domain f = domain g by move: oa oa1 => [_ s1 _] [_ s2 _]; ue. set E := (substrate (order_sum r g)). set F := (disjointU_fam (fam_of_substrates f)). have p1: partition_w_fam F (substrate (order_sum r f)). rewrite orsum_sr // /F /sum_of_substrates /disjointU. apply: partition_disjointU; rewrite /fam_of_substrates; fprops. have p3: (domain F = domain f). by rewrite /F/disjointU_fam /fam_of_substrates; aw. set di:= fun i => ((substrate (Vg f i)) *s1 i). set sj:= fun i => Lf (fun z => J (Vf (si i) (P z)) i) (di i) E. have p0: forall i, inc i (domain f) -> lf_axiom (fun z => J (Vf (si i) (P z)) i) (di i) E. move=> i idf z zV. move: (sip _ idf) => [_ _ [ff sf tf] _]. have aux: inc (Vf (si i) (P z) ) (substrate (Vg g i)). Wtac;move: zV => /indexed_P [_ Ps _]; ue. rewrite /E orsum_sr //; apply: disjoint_union_pi1 => //; ue. have FP: forall i, inc i (domain f) -> Vg F i = di i. move=> i idf; rewrite /F /disjointU_fam/fam_of_substrates Lgd !LgV//. have p2: forall i, inc i (domain F) -> function_prop (sj i) (Vg F i) E. rewrite p3;move=> i idf; rewrite /sj FP => //; aw. by saw;apply: lf_function; apply: p0. move: (extension_partition1 p1 p2). set G := common_ext _ _ _; move=> [[fG sG tG] alg]. rewrite p3 in alg. have aux: forall x, inc x (source G) -> [/\ inc (Q x) (domain f), inc x (di (Q x)), pairp x, inc (P x)(substrate (Vg f (Q x))) & Vf G x = J (Vf(si (Q x)) (P x)) (Q x)]. rewrite sG orsum_sr //; move => x xs; move: (du_index_pr1 xs)=> [Qxd Pxd px]. have xdi: inc x (di (Q x)) by apply /indexed_P;split => //. split => //. move: (alg _ Qxd); rewrite /agrees_on; move=> [q1 q2 q3]. move: (xdi); rewrite -FP // => q4. move: (q3 _ q4); rewrite /sj; rewrite LfV; aw;trivial;apply: p0 => //. exists G; split => //. move=> x y xs ys. move: (aux _ xs) (aux _ ys) => [Qx xdi px Px Wx][Qy ydi py Py Wy]. have qa: (sum_of_substrates f = source G) by rewrite sG orsum_sr. have qb: (sum_of_substrates g = target G) by rewrite tG /E orsum_sr //. split; move /orsum_gleP =>[q1 q2 q3]; apply /orsum_gleP. rewrite qb;split=> //; try Wtac; rewrite Wx Wy;red;aw; case: q3; first by left. move=> [Qxx le1]; right; split => //. rewrite -Qxx; move: (sip _ Qx) => [_ _ [_ sf tf] orf]. rewrite - orf //; rewrite sf //; ue. move: q3; rewrite /order_sum_r Wx Wy !pr2_pair !pr1_pair. move => q3; rewrite qa;split => //; case: q3; first by left. move=> [Qxx]; rewrite - {1} Qxx => le1; right; split => //. move: (sip _ Qx) => [_ _ [_ sf tf] orf]. apply /orf; rewrite ? sf //; ue. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)