proposition: Lemma csum_of_small_b5 f (s:= \csup (range f)) : fgraph f -> cardinal_fam f -> (exists i, [/\ inc i (range f), infinite_c i & cardinal (domain f) <=c i]) -> csum f = s.
proof: Proof. move => pa pa2 [i [ir l1 l2]]. have csr: cardinal_set (range f) by move=> t /(range_gP pa) [u ua ->]; apply: pa2. have pb:=(card_sup_ub csr ir). have pc := (cleT l2 pb). apply: csum_of_small_b4 => //. apply: (cle_inf_inf l1 pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)