proposition: Lemma fin_num_sume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I -> \bar R) : x \is a fin_num -> {in P &, forall i j, F i +? F j} -> x * (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) x * F i.
proof: Proof. move=> xfin PF; elim: s => [|h t ih]; first by rewrite !big_nil mule0. rewrite !big_cons; case: ifPn => Ph //. by rewrite muleDr// ?ih// adde_def_sum// => i Pi; rewrite PF. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed