proposition: Lemma cardinal_uniona X n: (forall x, inc x X -> cardinal x <=c n) -> cardinal (union X) <=c n *c cardinal X.
proof: Proof. move => h. set A := Lg (domain (identity_g X))(fun a => cardinal (Vg (identity_g X) a)). set B := cst_graph X n. have sd: domain A = domain B by rewrite /A/B identity_d; aw. have le:(forall x, inc x (domain A) -> Vg A x <=c Vg B x). rewrite /A/B Lgd identity_d => x xX; rewrite !LgV //; fprops. rewrite cprod2cr - csum_of_same. apply: cleT (csum_increasing sd le). by move: (csum_pr1 (identity_g X));rewrite setUb_identity. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)