proposition: Lemma isum_p7b (ps := fun n => (ipartial_sum (Zo E (fun t => glt r t n)))): has_greatest r \/ ipartial_sum E = \osup (fun_image E ps).
proof: Proof. case: (p_or_not_p (has_greatest r)); [ by left | move => nhg; right]. have ha: ordinalp (ipartial_sum E) by apply: isum_p1. have hb: ordinal_ub (fun_image E ps) (ipartial_sum E). move => y /funI_P [z ze ->]; rewrite /ps; apply: isum_p7a. move: (ord_ub_sup ha hb); case/ ole_eqVlt => //. set a := \osup _ => lab. have oa := (proj31_1 lab). move: (odiff_pr (proj1 lab)); set b := _ -o _; move =>[ob sab]. case: (equal_or_not b \0o) => bnz. by case: (proj2 lab); rewrite sab bnz (osum0r oa). move: (isum_p6 oa ob bnz sab). move =>[n [u [v [nE ou ov vnz [qa qb qc]]]]]. set I1 := (Zo E ((glt r)^~ n)). have i1p: I1 = segment r n. set_extens t; first by move /Zo_P => [sa sb]; apply/segmentP. move/segmentP => sa; apply/Zo_P; split => //. exact: (arg1_sr (proj1 sa)). move: (segmentc_pr (proj1 wor) nE). rewrite - i1p => eq2. have sa: sub I1 E by apply: Zo_S. have sb: sub (singleton n) E by move => t/set1_P ->. have sc i j: inc i I1 -> inc j (singleton n) -> glt r i j. by move=> /Zo_hi ma /set1_P ->. have sd: ordinalp (ipartial_sum I1) by apply: isum_p1. move: (isum_p4 sa sb sc); rewrite (isum_p3 nE) qa (osumA sd ou ov) - qb. set y := ipartial_sum (I1 +s1 n) => yv. have lay: a <o y. rewrite - yv; move: (osum_Meqlt (ord_ne0_pos ov vnz) oa). by rewrite(osum0r oa). have yT: inc y (fun_image E ps). have or := proj1 wor. have /(inc_segmentsP wor): segmentp r (I1 +s1 n). rewrite eq2; apply: (segmentc_segment _ or). case/setU1_P. move/funI_P => [m mE mv]; apply/funI_P; exists m => //. rewrite /y /ps; apply: f_equal; rewrite mv; set_extens t. move/segmentP => lt; apply:Zo_i => //;exact: (arg1_sr (proj1 lt)). by move/Zo_hi => lt; apply/segmentP. move => eq;case : nhg; exists n; split;rewrite - eq; fprops. by move => x/setU1_P; case; [ move/Zo_hi/proj1 | move ->; order_tac]. have os: ordinal_set (fun_image E ps). move => t /funI_P [m mE ->]; apply: isum_p1; apply: Zo_S. by case: (oleNgt (ord_sup_ub os yT)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)