proposition: Lemma csum_Cn2 J g I f : quasi_bij f I J -> csumb J g = csumb I (fun z => (g (f z))).
proof: Proof. move=> h; move:(quasi_bij_prop g h) => [tF bF vF]. rewrite /csumb (csum_Cn tF bF) vF; apply:csumb_exten. by move => i iI /=; rewrite LgV//; apply: (proj31 h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)