proposition: Lemma expr_sum {R : ringType} {T : Type} (x : R) (F : T -> nat) P s : x ^+ (\sum_(i <- s | P i) F i) = \prod_(i <- s | P i) x ^+ (F i).
proof: Proof. by apply: big_morph; [exact: exprD | exact: expr0]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)