proposition: Lemma aleph_sum_pr5 x: limit_ordinal x -> \aleph x = csumb x \aleph.
proof: Proof. by move => lx; apply:aleph_sum_pr4 => //;rewrite -[union _](limit_nonsucc lx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)