proposition: Lemma sum_of_sums f g I: (csumb I f) +c (csumb I g) = csumb I (fun i => (f i) +c (g i)).
proof: Proof. pose h i j := variant C0 (f i) (g i) j. move: (csum_An2 I C2 h). rewrite csum2_pr0. have ->: csumb I (h^~ C0) = csumb I f. by rewrite/h; apply:csumb_exten => i iI; rewrite variant_true1. have ->: csumb I (h^~ C1) = csumb I g. by rewrite/h; apply:csumb_exten => i iI; rewrite variant_false1. move <-. by apply:csumb_exten => i iI; rewrite csum2_pr0/h variant_true1 variant_false1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)