proposition: Lemma scaler_prodr (I : finType) (S : pred I) (F : I -> R) x : \prod_(i in S) (F i *: x) = \prod_(i in S) F i *: x ^+ #|S|.
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)