proposition: Lemma csum_of_small_b3 x f: csum_of_small1 x f -> (exists2 n, ordinalp n & x = \aleph (osucc n)) -> (cardinal (domain f)) <c x -> (csum f) <c x.
proof: Proof. move=> [pa pb] [n on xv] zx. rewrite xv in zx. move: (aleph_pr10a on zx) => le1. have pe: (allf f (cardinal_le ^~ (\omega n))). move=> i /pb; rewrite xv; apply: (aleph_pr10a on). move: (csum_of_small_b1 (conj pa pe)) => le2. move: (cprod_inf1 le1 (CIS_aleph on)); rewrite cprod2cr => le3. rewrite xv; exact (cle_ltT (cleT le2 le3) (aleph_pr10c on)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)