proposition: Lemma csum_gr f: csumb (domain f) (Vg f) = csum f.
proof: Proof. congr cardinal; rewrite /disjointU /disjointU_fam; aw. by congr unionb; apply:Lg_exten => x xdf; rewrite !LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)