proposition: Lemma sumZ S c : sum (c \*o S) = c * sum S.
proof: Proof. rewrite (eq_sum (F2 := fun x => Num.sg c * (`|c| * S x))). by move=> x; rewrite mulrA -numEsg. transitivity (Num.sg c * sum (`|c| \*o S)). case: sgrP => [_|gt0_c|lt0_c]; rewrite ?Monoid.simpm. + by rewrite (eq_sum (F2 := fun _ => 0)) ?sum0 // => x; rewrite !mul0r. + by apply/eq_sum=> x; rewrite mul1r. by rewrite mulN1r -sumN; apply/eq_sum=> x; rewrite !mulN1r. rewrite {1}/sum !(eq_psum (fposZ _ _), eq_psum (fnegZ _ _)) //. by rewrite !psumZ // -mulrBr mulrA -numEsg. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology