proposition: Lemma le0_sume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I -> \bar R) : (forall i, P i -> F i <= 0) -> (\sum_(i <- s | P i) F i) * x = \sum_(i <- s | P i) (F i * x).
proof: Proof. elim: s x P F => [x P F F0|h t ih x P F F0]; first by rewrite 2!big_nil mul0e. rewrite big_cons; case: ifPn => Ph; last by rewrite big_cons (negbTE Ph) ih. by rewrite le0_muleDl ?sume_le0// ?F0// ih// big_cons Ph. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed