proposition: Lemma aleph_sum_pr3 x: ordinalp x -> \aleph x = csumb (osucc x) \aleph.
proof: Proof. move=> ox. set f:= (Lg (osucc x) \aleph). have fgf: fgraph f by rewrite /f; fprops. have tdf: (x +s1 x) = (domain f) by rewrite /f; aw. have sd: sub (x +s1 x) (domain f) by rewrite tdf; apply: sub_refl. have ni: not (inc x x) by apply: (ordinal_irreflexive ox). move: (induction_sum0 f ni); rewrite /csumb. have ->: restr f (x +s1 x) = f by rewrite tdf restr_to_domain //. move=> ->; rewrite {2} /f LgV//; last by rewrite /osucc; fprops. suff: (csum (restr f x)) <=c (\aleph x). move=> h; symmetry; rewrite csumC; apply: csum_inf => //. by apply: CIS_aleph. rewrite (aleph_sum_pr2 ox) /csumb. set A := csum _; set B := csum _. suff ab: A <=c B. apply: (cleT ab); apply: (csum_Mle0 _ (proj32 ab)). have s1: sub x (osucc x) by rewrite /osucc; fprops. have sxd: sub x (domain f) by rewrite - tdf; fprops. have dr: (domain (restr f x)) = x by aw. apply: csum_increasing; aw; fprops. move=> y yx; rewrite /f !LgV//; last by apply: s1. by apply: aleph_le_lec; move: (oltS (Os_ordinal ox yx)) => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)