proposition: Lemma csum_pr1_bnd X f c: (forall i, inc i X -> cardinal (f i) <=c c) -> cardinal (unionf X f) <=c c *c X.
proof: Proof. move => H. move: (csum_pr1 (Lg X f)). have ->: unionb (Lg X f) = unionf X f. rewrite /unionb; aw;apply:setUf_exten => x xs;rewrite LgV//. rewrite /csumb Lgd - csum_of_same. set f1 := Lg _ _ => l1. set f2 := cst_graph X c. have sd: domain f1 = domain f2 by rewrite /f1/f2/cst_graph; aw. have pb: (forall x, inc x (domain f1) -> Vg f1 x <=c Vg f2 x). by rewrite /f1/f2/cst_graph;aw => x xa; rewrite !LgV//; apply:H. exact: (cleT l1 (csum_increasing sd pb)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)