proposition: Lemma csumA_setU2 A B f: disjoint A B -> csumb (A \cup B) f = csumb A f +c csumb B f.
proof: Proof. move => /(partition_setU2 f) dab; rewrite /csumb. rewrite (csum_An dab) variantLc_d csum2_pr0; aw. apply: f_equal2; apply: csumb_exten => i ia;rewrite LgV; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)