proposition: Lemma prodrMl {R : comRingType} {I : finType} (A : pred I) (x : R) F : \prod_(i in A) (x * F i) = x ^+ #|A| * \prod_(i in A) F i.
proof: Proof. rewrite -sum1_card; elim/big_rec3: _; first by rewrite expr0 mulr1. by move=> i y p z iA ->; rewrite mulrACA exprS. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)