proposition: Lemma scaler_prod I r (P : pred I) (F : I -> R) (G : I -> A) : \prod_(i <- r | P i) (F i *: G i) = \prod_(i <- r | P i) F i *: \prod_(i <- r | P i) G i.
proof: Proof. elim/big_rec3: _ => [|i x a _ _ ->]; first by rewrite scale1r. by rewrite -scalerAl -scalerAr scalerA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)