proposition: Lemma aleph_sum_pr4 x E: limit_ordinal x -> sub E x -> \csup E = x -> \aleph x = csumb E \aleph.
proof: Proof. move=> [pa pb pc] Ex sE. rewrite /csumb;set f := (Lg E \aleph); set y := csum f. have Ep: forall i, inc i E -> \aleph i <c \aleph x. by move=> i ie; apply:aleph_lt_ltc ;apply /(oltP pa) /Ex. have cf: cardinal_fam f. rewrite /f; hnf; aw; move=> i id; rewrite LgV//;exact: (proj31_1(Ep _ id)). apply: cleA; last first. have pd: csum_of_small1 (\aleph x) f. rewrite /f;split;fprops; hnf; aw => i id; rewrite LgV//; exact (Ep _ id). move: (csum_of_small_b2 pd); rewrite {2} /f Lgd - cprod2cr. move: (sub_smaller (sub_trans Ex (proj33 (aleph_pr6 pa)))). rewrite (card_card (CS_aleph pa)). move=> qa qb; exact: (cleT qb(cprod_inf1 qa (CIS_aleph pa))). have yg: forall t, inc t E -> \aleph t <=c y. move=> t tE; have tdf: inc t (domain f) by rewrite /f Lgd. move: (csum_increasing6 (cf _ tdf) tdf); rewrite /f LgV//. have osE: ordinal_set E by move=> t tE; exact (Os_ordinal pa (Ex _ tE)). have iy: infinite_c y. case: (emptyset_dichot E). move=> ee; move: pb; rewrite - sE ee setU_0; case; case. move=> [t tE]; move: (yg _ tE) => le2. exact: (cle_inf_inf (CIS_aleph (osE _ tE)) le2). move: (ord_index_pr1 iy) => [];set z := (ord_index y) => oz yv. rewrite - yv; apply: aleph_le_lec. rewrite - sE; apply: ord_ub_sup => //. move=> t te; move: (yg _ te); rewrite -yv=> h; move: (ocle h). apply: aleph_leo_le => //; exact (osE _ te). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)