proposition: Lemma isum_p4 I1 I2: sub I1 E -> sub I2 E -> (forall i j, inc i I1 -> inc j I2 -> glt r i j) -> (ipartial_sum I1) +o (ipartial_sum I2) = ipartial_sum (I1\cup I2).
proof: Proof. move => E1N E2N lE1E2. have E12N: sub (I1 \cup I2) E by apply: setU2_12S. move:(fprop) =>[ha hb hc]. rewrite 3! isum_p0. move:(isum_q2 E1N) (isum_q2 E2N) (proj1 (isum_q2 E12N)). move:(isum_q5 E1N) (isum_q5 E2N) (isum_q5 E12N). set s1 := ipartial_order _; set s2 := ipartial_order _; set s3:= ipartial_order _. move => sr1 sr2 sr3 wor1 wor2 or3. apply: (orsum_invariant5 wor1 wor2). move: (orsum2_osr (proj1 wor1) (proj1 wor2)) =>[or4 sr4]. have ax: lf_axiom P (dsum (substrate s1) (substrate s2)) (substrate s3). rewrite sr1 sr2 sr3;move => t /candu2P [pt]; case; case. by move/isum_q6=>[qa qb qc] qd; apply/isum_q6; split => //; apply: setU2_1. by move/isum_q6=>[qa qb qc] qd; apply/isum_q6; split => //; apply: setU2_2. have qa a: inc a (substrate s1) -> inc (Q a) I1. by rewrite sr1 => /disjointU_P/proj31; aw. have qb a: inc a (substrate s2) -> inc (Q a) I2. by rewrite sr2 => /disjointU_P/proj31; aw. have bp: bijection_prop (Lf P (substrate (order_sum2 s1 s2)) (substrate s3)) (substrate (order_sum2 s1 s2)) (substrate s3). saw; rewrite sr4; apply: lf_bijective; first exact. move => x y /candu2P [px qx] /candu2P [py qy] sp; apply: pair_exten => //. case: qx; case: qy; move =>[sa ->][sc ->] //. by case: (proj2 (lE1E2 _ _ (qa _ sc) (qb _ sa))); rewrite sp. by case: (proj2 (lE1E2 _ _ (qa _ sa) (qb _ sc))); rewrite sp. rewrite sr3; move => y /disjointU_P []; rewrite Lgd => qd. rewrite LgV// => qe qf; case /setU2_P: qd => qd. exists (J y C0);aw;trivial;apply:candu2_pra; rewrite sr1. by apply/disjointU_P; aw; rewrite LgV. exists (J y C1); aw;trivial; apply:candu2_prb;rewrite sr2. by apply/disjointU_P; aw; rewrite LgV. suff : fiso_prop (Lf P (substrate (order_sum2 s1 s2)) (substrate s3)) (order_sum2 s1 s2) s3. by move => iso; exists (Lf P (substrate (order_sum2 s1 s2)) (substrate s3)). hnf; aw; rewrite sr4 => x y xd yd; rewrite !LfV//. move/candu2P:(xd) => [px qx]; move/candu2P: (yd) => [py qy]. split. move/orsum2_gleP =>[_ _ etc]. apply/(isum_q7 E12N); rewrite - (isum_q5 E12N); split; fprops. case: etc. - by move =>[sa sb sc]; move/(isum_q7 E1N): sc => /proj33. - by move =>[sa sb sc]; move/(isum_q7 E2N): sc => /proj33. - move => [pa pb];case: qx;case; last by rewrite pa => _ h; case: C0_ne_C1. move => ps1 _ ; case: qy; case => // ps2 _. left; move:(qa _ ps1) (qb _ ps2) => pe qe; exact: (lE1E2 _ _ pe qe). move/(isum_q7 E12N) => [_ _ h]; apply/orsum2_gleP; split => //. move: (isum_q5 E1N) (isum_q5 E2N) => a1 a2. case: h. move => h. case: qx; case: qy; move =>[sa sb][sc sd]. - constructor 1; split => //; apply/(isum_q7 E1N). by rewrite - a1; split => //; left. - constructor 3; split => //; rewrite sb; fprops. - case: (not_le_gt (proj1 wor) (proj1 h) (lE1E2 _ _ (qa _ sa) (qb _ sc))). - constructor 2; rewrite sd sb; split; fprops; apply/(isum_q7 E2N). by rewrite - a2; split => //; left. move => [sx sy]. case: qx; case: qy; move =>[sa sb][sc sd]. - constructor 1; split => //;apply/(isum_q7 E1N). by rewrite - a1; split => //; right. - constructor 3; split => //; rewrite sb; fprops. - by case : (proj2 (lE1E2 _ _ (qa _ sa) (qb _ sc))). - constructor 2; rewrite sd sb; split; fprops; apply/(isum_q7 E2N). by rewrite - a2; split => //; right. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)