proposition: Lemma csum_pr3 f g: domain f = domain g -> (forall i, inc i (domain f) -> Vg f i =c Vg g i) -> csum f = csum g.
proof: Proof. by move=> dfg sc; rewrite 2!csum_pr -dfg; apply:csumb_exten. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)