proposition: Lemma scaler_prodl (I : finType) (S : pred I) (F : I -> A) k : \prod_(i in S) (k *: F i) = k ^+ #|S| *: \prod_(i in S) F i.
proof: Proof. by rewrite scaler_prod prodr_const. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)