proposition: Lemma psumZr S c : 0 <= c -> psum (c \o* S) = psum S * c.
proof: Proof. move=> ge0_c; rewrite [RHS]mulrC -psumZ //. by apply/eq_psum => x /=; rewrite mulrC. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology