proposition: Lemma isum_p6 a b: ordinalp a -> ordinalp b -> b <> \0o -> ipartial_sum E = a +o b -> exists n u v, [/\ inc n E, ordinalp u, ordinalp v, v <> \0o & [/\ Vg f n = u +o v, a = (ipartial_sum (Zo E (fun t => glt r t n))) +o u & b = v +o (ipartial_sum (Zo E (fun t => glt r n t))) ]].
proof: Proof. move => oa ob bnz. have or := (proj1 wor). move: (fprop) => [fgf df ofs]. move: C0_ne_C1 C1_ne_C0 => nea neb. pose oE E := ipartial_order E. pose oxy x y := (order_sum2 (ordinal_o x) (ordinal_o y)). rewrite {1} /osum2 isum_p0-/(oE E) -/(oxy _ _). set osig := oE E. set oab := oxy a b => eqa. have Hu c: ordinalp c -> forall x y, inc x c -> inc y c -> (gle (ordinal_o c) x y <-> x <=o y). move => oc x y xc yc; split. by move/ordo_leP =>[_ _ s]; split => //; apply: (Os_ordinal oc). by move => /proj33 s; apply/ordo_leP. have He x y: ordinalp x -> ordinalp y -> worder (oxy x y). move => /ordinal_o_wor xa /ordinal_o_wor xb. by apply:orsum2_wor. have Ha x y: ordinalp x -> ordinalp y -> substrate (oxy x y) = dsum x y. move => /ordinal_o_wor/proj1 qa /ordinal_o_wor/proj1 qb. by rewrite (orsum2_sr qa qb) ! ordinal_o_sr. have wosig : worder osig by apply: isum_q2. have woab: worder oab by apply: He. move:(Ha _ _ oa ob); rewrite -/oab => soab. have sosig : substrate osig = disjointU f. by rewrite isum_q5 // -df restr_to_domain. have: oab \Is osig. move: (ordinal_o_is woab); rewrite - eqa => is1. exact: (orderIT is1 (orderIS (ordinal_o_is wosig))). move =>[g [o1 o2 [bg sg tg] gm]]. have fg := proj1 (proj1 bg). have zb: inc \0o b by apply/(oltP ob); apply: ord_ne0_pos. have ha: inc (J \0o C1) (source g). by rewrite sg soab; apply: candu2_prb. move: (Vf_target fg ha). rewrite tg sosig; move/setUf_P. rewrite/disjointU_fam; rewrite df; aw; move => [n nN]; rewrite LgV//. set xr := Vf g (J \0o C1) => hb. move/indexed_P:(hb) => [hb1 hb2 hb3]. set u := (P xr). have oan: ordinalp (Vg f n). by apply:ofs; ue. have lt1: u <o (Vg f n) by apply/oltP. have ou := proj31_1 lt1. move:(odiff_pr (proj1 lt1)); set v := _ -o _; move => [ov eq2]. case: (equal_or_not v \0o) => vnz. by move: (proj2 lt1); rewrite eq2 vnz (osum0r ou). exists n,u,v. set w1 := ipartial_sum _. set w2 := ipartial_sum _. have w1p: sub (Zo E ((glt r)^~ n)) E. by apply: Zo_S. have w2p: sub (Zo E [eta glt r n]) E by apply: Zo_S. have ow1: ordinalp w1 by apply: isum_p1. have ow2: ordinalp w2 by apply: isum_p1. have rb x: inc x b -> gle osig xr (Vf g (J x C1)). move => xb. have xs: inc (J x C1) (source g) by rewrite sg soab; apply: candu2_prb. apply/(gm _ _ ha xs);apply/(isum_q8 oa ob); rewrite - soab - sg;split => //. constructor 2; aw; split => //; apply: ole0x; apply(Os_ordinal ob xb). have ra x: inc x a -> glt osig (Vf g (J x C0)) xr. move => xb. have xs: inc (J x C0) (source g) by rewrite sg soab; apply: candu2_pra. split; last first. by move/(proj2 (proj1 bg) _ _ xs ha) /pr2_def. apply/(gm _ _ xs ha);apply/(isum_q8 oa ob);rewrite - soab - sg;split => //. by constructor 3; aw. move: (proj2 (proj2 bg)); rewrite sg tg sosig soab => sjg. have <- : b = v +o w2. rewrite -(ordinal_o_o ob). move:(ordinal_o_wor ob) (He _ _ ov ow2) => wo1 wo2. apply:(ordinal_o_isu1 wo1 wo2); move: wo1 wo2 => [oo1 _] [oo2 _]. move:(Ha _ _ ov ow2) => sr2. move: (isum_q2 w2p) (isum_q5 w2p); set o3 := ipartial_order _ => wo3 sr3. have xx: ordinal o3 = w2 by rewrite /w2 isum_p0. move: (ordinal_o_is wo3); rewrite xx => is1; clear xx. move: is1 =>[f3 [or1 or2] [bf3 sf3 tf3] f3m]. have ff3 := proj1 (proj1 bf3). rewrite ordinal_o_sr in tf3. rewrite sr3 in sf3. pose h x := let y := (Vf g (J x C1)) in Yo (Q y = n) (J ((P y) -o u) C0) (J (Vf f3 y) C1). have ax: lf_axiom h b (dsum v w2). move => x /rb; rewrite /h; set y := Vf _ _. move => /(isum_q7 (@sub_refl E)) [qa qb qc]. move/isum_q6: qb =>[sa sb sc]. case: qc. rewrite hb3 => lt2; rewrite (Y_false (nesym (proj2 lt2))). apply: candu2_prb. by Wtac; rewrite sf3; apply/isum_q6; split => //; apply:(Zo_i sa). rewrite hb3; move =>[ea se]; rewrite ea; Ytac0; apply: candu2_pra. apply/(oltP ov); rewrite - ea in sb; move/(oltP oan): sb; rewrite eq2. move:(odiff_pr se) => [ma mb]; rewrite {1} mb;exact:(osum_Meqltr ma ov ou). have Ta x: inc x b -> Q (Vf g (J x C1)) <> n -> inc (Vf g (J x C1)) (source f3). move => xa; move/(isum_q7 (@sub_refl E)) : (rb x xa). rewrite sf3; move => [_ /isum_q6 [qa qb qc]]; case. move => [ta tb] tc; apply/isum_q6; split => //. by apply: (Zo_i qa); split => //; rewrite - hb3. by move/proj1 => <-; rewrite hb3. have bp: bijection (Lf h b (dsum v w2)). apply: lf_bijective => //. move => x y xa ya; rewrite /h => aux. suff: (J x C1) = (J y C1) by apply: pr1_def. have xd: inc (J x C1) (dsum a b) by apply: candu2_prb. have yd: inc (J y C1) (dsum a b) by apply: candu2_prb. have xsg: inc (J x C1) (source g) by rewrite sg soab. have ysg: inc (J y C1) (source g) by rewrite sg soab. apply: (proj2 (proj1 bg) _ _ xsg ysg); move: aux. rewrite /h; set z1 := Vf g _; set z2 := Vf g _;Ytac na; Ytac nb. + move/rb: xa => /(isum_q7 (@sub_refl E)) /proj33; case. by move/proj2; rewrite na hb3. move/rb: ya => /(isum_q7 (@sub_refl E)) /proj33; case. by move/proj2; rewrite nb hb3. rewrite -/z1 -/z2 -/u; move => [_ le1] [_ le2]. move: (Vf_target fg xsg) (Vf_target fg ysg). rewrite tg sosig; move => /disjointU_P => /proj33 px. move => /disjointU_P => /proj33 py /pr1_def sd. apply: pair_exten => //; last by rewrite na nb. by move: (odiff_pr le1) (odiff_pr le2) =>[ma ->][mc ->]; rewrite sd. + by move => /pr2_def. + by move => /pr2_def. + by move => /pr1_def; apply: (proj2 (proj1 bf3)); apply: Ta. move => y /candu2P [pp]; case; move => [sa sb]. move/(oltP ov): (sa) => sc. move: (odiff_pr1 ou (proj31_1 sc)) => sd. have: inc (J (u +o (P y)) n) (disjointU f). apply/disjointU_P; aw; rewrite df; split; fprops. apply/(oltP oan); rewrite eq2. apply: (osum_Meqlt _ ou). by apply/(oltP ov). move/sjg =>[z zab -zv]. move/candu2P: zab => [pz]; case; move =>[zu zw]. move: (ra _ zu); rewrite - zw pz - zv. move/(isum_q7_lt (@sub_refl E)) =>[_ h3]; rewrite hb3; aw. move: (osum_Mle0 ou (proj31_1 sc)) => ll. by case; case => // _ /oltNge; case. exists (P z) => //; rewrite /h - zw pz - zv - sb; aw; Ytac0. by rewrite sd pp. rewrite - tf3 in sa; move: (proj2 (proj2 bf3) _ sa); rewrite sf3. move => [x /isum_q6 [/Zo_P [qa qb] qc] qd] qe. have: inc x (disjointU f) by apply/disjointU_P; split => //; ue. move /sjg =>[z zab -zv]. move/candu2P: zab => [pz]; case; move =>[zu zw]. move: (ra _ zu); rewrite - zw pz - zv. move/(isum_q7_lt (@sub_refl E)) =>[_ h3]; rewrite hb3; case. by move=> h4; move: (not_le_gt or (proj1 qb) h4). by move => [nn]; case (proj2 qb). exists (P z) => //; rewrite /h - zw pz - zv (Y_false (nesym (proj2 qb))). by rewrite zw - sb - qe pp. exists (Lf h b (dsum v w2)). have tor:= (worder_total (ordinal_o_wor ob)). apply: total_order_isomorphism; aw;trivial; first by rewrite ordinal_o_sr. hnf => x y xa ya /=; rewrite !LfV //; move => lea. have xd: inc (J x C1) (dsum a b) by apply: candu2_prb. have yd: inc (J y C1) (dsum a b) by apply: candu2_prb. have xsg: inc (J x C1) (source g) by rewrite sg soab. have ysg: inc (J y C1) (source g) by rewrite sg soab. have /(gm _ _ xsg ysg) lb: gle oab (J x C1) (J y C1). apply/(isum_q8 oa ob); split => //; constructor 2; aw. by split=> //; apply/(Hu _ ob _ _ xa ya). move/(isum_q7 (@sub_refl E)): lb. rewrite /h; set z1 := (Vf g (J x C1)); set z2 := (Vf g (J y C1)). move: (rb _ xa); rewrite -/z2 => /(isum_q7 (@sub_refl E)). move/proj33; rewrite hb3 -/u; move => z1prop. have f3sm s t: inc s (source f3) -> inc t (source f3) -> ((glt r (Q s) (Q t) \/ Q s = Q t /\ P s <=o P t) <-> Vf f3 s <=o Vf f3 t). move => ss ts. move: (Vf_target ff3 ss) (Vf_target ff3 ts); rewrite tf3 => sw tw. apply: iff_trans (iff_trans (f3m s t ss ts) (Hu _ ow2 _ _ sw tw)). have aux: sub (Zo E ((glt r) n)) E by apply: Zo_S. split; last by case /(isum_q7 aux). by move => H; apply/(isum_q7 aux); rewrite - sf3. move => [pa pb]. move/isum_q6: (pa) => [z11 z12 z13]. move/isum_q6: (pb) => [z21 z22 z23]. case. move => lt12; case: z1prop. move => lt2n; move: (lt_lt_trans or lt2n lt12) => lt1n. rewrite (Y_false (nesym (proj2 lt1n))) (Y_false (nesym (proj2 lt2n))). have z1f3: inc z1 (source f3). by rewrite sf3; apply/isum_q6; split => //; apply: Zo_i => //. have z2f3: inc z2 (source f3). by rewrite sf3; apply/isum_q6; split => //; apply: Zo_i => //. apply/(isum_q8 ov ow2); split. - apply: candu2_prb; Wtac. - apply: candu2_prb; Wtac. - by constructor 2; aw; split=>//; apply/(f3sm z1 z2 z1f3 z2f3); left. move => [ea la]; rewrite ea -/z1 (Y_false (nesym (proj2 lt12))); Ytac0. apply/(isum_q8 ov ow2); split. - apply: candu2_pra; move: (odiff_pr la) => [ma mb]. apply/(oltP ov); apply: (osum_Meqltr ma ov ou); rewrite - mb - eq2. by apply/(oltP oan); rewrite ea. - apply: candu2_prb; Wtac; rewrite sf3; apply/isum_q6; split => //. apply: Zo_i => //; ue. - by constructor 3; aw. move => [pc pd]; case: z1prop. move => lt2n; rewrite - pc 2! (Y_false (nesym (proj2 lt2n))). have z1f3: inc z1 (source f3). by rewrite sf3;apply/isum_q6; split => //; apply: Zo_i => //; ue. have z2f3: inc z2 (source f3). rewrite sf3; apply/isum_q6; split => //; apply: Zo_i => //; ue. apply/(isum_q8 ov ow2); split. - apply: candu2_prb; Wtac. - apply: candu2_prb; Wtac. - by constructor 2; saw; apply/(f3sm z1 z2 z1f3 z2f3); right. move => [ea la]; rewrite - pc - ea; Ytac0; Ytac0. move: (oleT la pd) => lb. move: (odiff_pr la) (odiff_pr lb) => [ma mb] [mc md]. have aux: P z1 -o u <=o P z2 -o u. by apply:(osum_Meqler ma mc ou); rewrite - mb - md. apply/(isum_q8 ov ow2); split. - apply: candu2_pra; apply/(oltP ov); apply:(osum_Meqltr ma ov ou). by rewrite - mb - eq2; apply/(oltP oan); rewrite ea. - apply: candu2_pra; apply/(oltP ov); apply:(osum_Meqltr mc ov ou). by rewrite - md - eq2; apply/(oltP oan); rewrite ea pc. - by constructor 1; aw. suff <- : a = w1 +o u by split. rewrite -(ordinal_o_o oa). move:(ordinal_o_wor oa) (He _ _ ow1 ou) => wo1 wo2. apply:(ordinal_o_isu1 wo1 wo2); move: wo1 wo2 => [oo1 _] [oo2 _]. move:(Ha _ _ ow1 ou) => sr2. move: (isum_q2 w1p) (isum_q5 w1p); set o3 := ipartial_order _ => wo3 sr3. have xx: ordinal o3 = w1 by rewrite /w1 isum_p0. move: (ordinal_o_is wo3); rewrite xx => is1; clear xx. move: is1 =>[f3 [or1 or2] [bf3 sf3 tf3] f3m]. have ff3 := proj1 (proj1 bf3). rewrite ordinal_o_sr in tf3. rewrite sr3 in sf3. pose h x := let y := (Vf g (J x C0)) in Yo (Q y = n) (J (P y) C1) (J (Vf f3 y) C0). have suan: sub u (Vg f n). move => t /(oltP ou) => ltu; apply/(oltP oan); rewrite eq2. by apply: (olt_leT ltu (osum_Mle0 ou ov)). have ax: lf_axiom h a (dsum w1 u). move => x /ra; rewrite /h; set y := Vf _ _. move => /(isum_q7_lt (@sub_refl E)) [qa qb qc]. move/isum_q6: qa =>[sa sb sc]. case: qc. rewrite hb3 => lt2; rewrite (Y_false (proj2 lt2)); apply: candu2_pra. by Wtac; rewrite sf3; apply/isum_q6; split => //; apply:(Zo_i sa). rewrite hb3; move =>[sd se]; Ytac0; apply: candu2_prb. by apply/(oltP ou). have Ta x: inc x a -> Q (Vf g (J x C0)) <> n -> inc (Vf g (J x C0)) (source f3). move => xa; move/(isum_q7_lt (@sub_refl E)) : (ra x xa). rewrite sf3; move => [/isum_q6 [qa qb qc] _]; case. move => [ta tb] tc; apply/isum_q6; split => //. apply: (Zo_i qa); split => //; ue. by rewrite hb3; case. have bp: bijection (Lf h a (dsum w1 u)). apply: lf_bijective => //. move => x y xa ya; rewrite /h => aux. suff: (J x C0) = (J y C0) by apply: pr1_def. have xd: inc (J x C0) (dsum a b) by apply: candu2_pra. have yd: inc (J y C0) (dsum a b) by apply: candu2_pra. have xsg: inc (J x C0) (source g) by rewrite sg soab. have ysg: inc (J y C0) (source g) by rewrite sg soab. apply: (proj2 (proj1 bg) _ _ xsg ysg); move: aux. rewrite /h; set z1 := Vf g _; set z2 := Vf g _;Ytac na; Ytac nb. + move: (Vf_target fg xsg) (Vf_target fg ysg). rewrite tg sosig; move => /disjointU_P => /proj33 px. move => /disjointU_P => /proj33 py. move => /pr1_def ee; apply: pair_exten => //; ue. + by move => /pr2_def. + by move => /pr2_def. + by move => /pr1_def; apply: (proj2 (proj1 bf3)); apply: Ta. move => y /candu2P [pp]; case; move => [sa sb]. rewrite - tf3 in sa; move: (proj2 (proj2 bf3) _ sa); rewrite sf3. move => [x /isum_q6 [/Zo_P [qa qb] qc] qd] qe. have: inc x (disjointU f) by apply/disjointU_P; split => //; ue. move /sjg =>[z zab -zv]. move/candu2P: zab => [pz]; case; move =>[zu zw]. exists (P z) => //; rewrite /h - zw pz - zv (Y_false (proj2 qb)). by rewrite zw - sb - qe pp. move: (rb _ zu); rewrite - zw pz - zv. move/(isum_q7 (@sub_refl E)) =>[_ h3]; rewrite hb3; case. by move=> h4; move: (not_le_gt or (proj1 qb) h4). by move => [nn]; case (proj2 qb). have: inc (J (P y) n) (disjointU f). by apply/disjointU_P; aw; rewrite df; split; fprops; apply: suan. move/sjg =>[z zab -zv]. move/candu2P: zab => [pz]; case; move =>[zu zw]. by exists (P z)=>//; rewrite /h - zw pz - zv - sb; aw; Ytac0; rewrite pp. move: (rb _ zu); rewrite - zw pz - zv. move/(isum_q7 (@sub_refl E)) =>[_ h3]; rewrite hb3; aw; case; case => //. by move => _ /oleNgt; case; apply/(oltP ou). exists (Lf h a (dsum w1 u)). have tor:= (worder_total (ordinal_o_wor oa)). apply: total_order_isomorphism; aw; trivial;first by rewrite ordinal_o_sr. hnf => x y xa ya /=; rewrite !LfV//; move => lea. have xd: inc (J x C0) (dsum a b) by apply: candu2_pra. have yd: inc (J y C0) (dsum a b) by apply: candu2_pra. have xsg: inc (J x C0) (source g) by rewrite sg soab. have ysg: inc (J y C0) (source g) by rewrite sg soab. have /(gm _ _ xsg ysg) lb: gle oab (J x C0) (J y C0). apply/(isum_q8 oa ob); split => //; constructor 1; aw. by split=> //; apply/(Hu _ oa _ _ xa ya). move/(isum_q7 (@sub_refl E)): lb. rewrite /h; set z1 := (Vf g (J x C0)); set z2 := (Vf g (J y C0)). move: (ra _ ya); rewrite -/z2 => /(isum_q7_lt (@sub_refl E)). move/proj33; rewrite hb3 -/u; move => z2prop. have f3sm s t: inc s (source f3) -> inc t (source f3) -> ((glt r (Q s) (Q t) \/ Q s = Q t /\ P s <=o P t) <-> Vf f3 s <=o Vf f3 t). move => ss ts. move: (Vf_target ff3 ss) (Vf_target ff3 ts); rewrite tf3 => sw tw. apply: iff_trans (iff_trans (f3m s t ss ts) (Hu _ ow1 _ _ sw tw)). have aux: sub (Zo E ((glt r)^~ n)) E by apply: Zo_S. split. by move => H; apply/(isum_q7 aux); rewrite - sf3. by case /(isum_q7 aux). move => [pa pb]. move/isum_q6: (pa) => [z11 z12 z13]. move/isum_q6: (pb) => [z21 z22 z23]. case. move => lt12; case: z2prop. move => lt2n; move: (lt_lt_trans or lt12 lt2n) => lt1n. rewrite (Y_false (proj2 lt1n))(Y_false (proj2 lt2n)). have z1f3: inc z1 (source f3). by rewrite sf3; apply/isum_q6; split => //; apply: Zo_i => //. have z2f3: inc z2 (source f3). by rewrite sf3; apply/isum_q6; split => //; apply: Zo_i => //. apply/(isum_q8 ow1 ou); split. - apply: candu2_pra; Wtac. - apply: candu2_pra; Wtac. - by constructor 1; aw; split=>//; apply/(f3sm z1 z2 z1f3 z2f3); left. move => [ea la]; rewrite - ea (Y_false (proj2 lt12)); Ytac0. apply/(isum_q8 ow1 ou); split. - apply: candu2_pra; Wtac; rewrite sf3; apply/isum_q6; split => //. apply: Zo_i => //; ue. - by apply: candu2_prb; apply/(oltP ou). - by constructor 3; aw. move => [pc pd]; case: z2prop. move => lt2n; rewrite pc 2! (Y_false (proj2 lt2n)). have z1f3: inc z1 (source f3). by rewrite sf3;apply/isum_q6; split => //; apply: Zo_i => //; ue. have z2f3: inc z2 (source f3). by rewrite sf3; apply/isum_q6; split => //; apply: Zo_i => //. apply/(isum_q8 ow1 ou); split. - apply: candu2_pra; Wtac. - apply: candu2_pra; Wtac. - by constructor 1; aw; split=>//; apply/(f3sm z1 z2 z1f3 z2f3); right. move => [ea la]; rewrite pc - ea; Ytac0; Ytac0. move: (ole_ltT pd la) => lb. apply/(isum_q8 ow1 ou); split. - by apply: candu2_prb; apply/(oltP ou). - by apply: candu2_prb; apply/(oltP ou). - by constructor 2; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)