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