proposition: Lemma mulr_suml I r P (F : I -> R) x : (\sum_(i <- r | P i) F i) * x = \sum_(i <- r | P i) F i * x.
proof: Proof. exact: big_distrl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)