proposition: Lemma csum_of_same a b: csumb b (fun i: Set => a) = a *c b.
proof: Proof. rewrite cprod2_pr1; congr cardinal; rewrite disjointU_E ;set_extens t. move=> /setUf_P [y yj]; aw. move => /indexed_P [pa pb pc]; apply /setX_P;split => //; ue. by move /setX_P => [pa pb pc]; apply/setUf_P; ex_tac; aw; apply/indexed_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)