proposition: Lemma aleph_sum_pr2 x: ordinalp x -> \aleph x = omega0 +c csumb x (fun z => \aleph (osucc z)).
proof: Proof. move=> ox. have /cardinal_setC: sub omega0 (\aleph x). by move: (aleph_pr5 ox) => [_ _]. rewrite (card_card (CS_aleph ox)) (card_card (CS_omega)). move => <-; congr (_ +c _); rewrite /cdiff. have oa := OS_aleph ox. have ->: ((\aleph x) -s omega0) = unionb (Lg x aleph_succ_comp). set_extens t. move /setC_P;move=> [pa pb]; move: (Os_ordinal oa pa) => ot. case: (aleph_sum_pr1 ot) => // [] [y oy ta]. move /(aleph_succ_P1 oy): (ta) => [pc pd]. suff yx: inc y x by apply /setUb_P; exists y; aw;trivial; rewrite LgV. have le1: t <o (\aleph x) by apply /oltP. by move:(aleph_lto_lt oy ox (ole_ltT pc le1)) => /oltP0[_ _]. move=> /setUb_P; aw; move => [y yx]; rewrite (LgV yx). move/(oltP ox): yx => yx. have oy:=proj31_1 yx. move/(aleph_succ_P1 oy) => [p1 p2]; apply /setC_P; split. move /oleSltP: yx => /(aleph_le_leo) ca. by move: (olt_leT p2 ca) => /oltP0 [_ _]. move: (oleT (aleph_pr5 oy) p1) => [q1 q2 q3] q4. exact: (ordinal_irreflexive q2 (q3 _ q4)). apply: Eqc_disjointU; last by fprops. hnf; rewrite /disjointU_fam; split;aww. move=> i ix; rewrite !LgV//; aw. have oi:= (Os_ordinal ox ix). rewrite (aleph_succ_pr2 oi) card_card //. exact:(CS_aleph (OS_succ oi)). red; aw; move=> i j ix jx; rewrite !LgV//. by apply: aleph_succ_pr3; apply: (Os_ordinal ox). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)