proposition: Lemma notbig_family_sum1 a f: infinite_c a -> (cardinal (domain f)) <=c a -> (forall i, inc i (domain f) -> (Vg f i) <=c a) -> (exists2 j, inc j (domain f) & (Vg f j) = a) -> csum f = a.
proof: Proof. move=> ifa leda alea [j0 j0d vj0]. apply: (cleA (notbig_family_sum ifa leda alea)). by rewrite -vj0; apply:csum_increasing6 j0d; rewrite vj0; case:ifa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)