proposition: Lemma csum_of_small_b4 f (s:= \csup (range f)) : fgraph f -> cardinal_fam f -> infinite_c s -> (cardinal (domain f) <=c s) -> csum f = s.
proof: Proof. move=> pa1 pa pb pc. have csr: cardinal_set (range f). by move=> t /(range_gP pa1) [u ua ->]; apply: pa. have pe: s *c domain f = s. rewrite - cprod2cr; apply: cprod_inf => //. apply: card_nonempty1. case: (emptyset_dichot (domain f)) => // de. move: (clt_fin_inf finite_0 pb) => [_]; rewrite /s. have -> :(range f = emptyset) by apply /range_set0_P; apply/domain_set0_P. by rewrite setU_0;case. apply: cleA. have pd: (allf f (cardinal_le ^~ s)). move=> i idf; apply: (card_sup_ub csr); apply /(range_gP pa1); ex_tac. by rewrite - pe; apply:(csum_of_small_b1 (conj pa1 pd)). apply: card_ub_sup => //; first by rewrite /csum; fprops. move => a /(range_gP pa1) [x xdf ->]; apply: csum_increasing6 =>//. by apply:pa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)